Papers 20 Years of Covert Channel Modeling and Analysis 31st Annual Simulation Symposium: High-fidelity Simulation of Local Area Networks Abstract and Model Check while you Prove Abstract Congruence Closure and Specializations Abstract Datatypes in PVS Abstract interpretation of probabilistic semantics An Abstract Monte-Carlo Method for the Analysis of An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs Abstracting cryptographic protocols with tree automata Acceptance of Formal Methods: Lessons from Hardware Design Accessing Information and Services on the DAML-Enabled Web An Adaptable Network COntrol and Reporting System (ANCORS) Adaptive Fault-Resistant Systems Adaptive, Model-based Monitoring for Cyber Attack Detection Analyzing Cockpit Interfaces Using Formal Methods Analyzing Tabular and State-Transition Specifications in PVS ANCORS: Adaptable Network Control and Reporting Systems Application Experience with an Implicitly Parallel Composition Language Application-Integrated Data Collection for Security Monitoring Applications of Term Rewriting to Cryptographic Protocol Analysis Applying Formal Evaluation to Worm Defense Design Applying Formal Verification to a Commercial Microprocessor Architectural Support for Copy and Tamper Resistant Software An Architecture for an Adaptive Intrusion Tolerant Server Architecture-Driven Software Component Retrieval Architectures and Formal Representations for Secure Systems Assessment and content authoring in semantically enabled virtual environments Associative-Commutative Rewriting on Large Terms Authenticating, Key Distribution, and Secure Broadcast in Computer Networks Using No Encryption or Descryption Automated Audit Trail Analysis and Intrusion Detection: A Survey Automated Code Generator Verification Based on Algebraic Laws Automated Deduction and Formal Methods Automated Deductive Verification of Parallel Systems An Automated Method To Detect Potential Mode Confusions Automatic Analysis of Firewall and Network Intrusion Detection System Configurations Automatic Verification of Parameterized Networks of Processes by Abstraction Automatically Deducing Propagation Sequences that Circumvent a Collaborative Worm Defense Avionics Systems Requirements: A Comparison of RSML and SCR Bonsai: Balanced Lineage Authentication Bounded Model Checking for Timed Automata Building Equational Proving Tools by Reflection in Rewriting Logic Bus Architectures For Safety-Critical Embedded Systems Byzantine Agreement with Authentication: Observations and Applications in Tolerating Hybrid and Link Faults Calculating with Requirements CAPSL and MuCAPSL A CAPSL Connector to Athena (Extended Abstract) CAPSL Integrated Protocol Environment CAPSL Interface for the NRL Protocol Analyzer CAPSL Intermediate Language A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs Certificate Revocation the Responsible Way Certifying and Synthesizing Membership Equational Proofs Certitude and Rectitude The Challenges of Insider Misuse Checking the Correctness of Architectural Transformation Steps via Proof-Carrying Architectures Clocked FSM Sythesis considering Real Time Constraints Cognitive Radio Policy Language and Policy Engine A Collaborative Programming Environment for Web Interoperability Combining monitors for run-time system verification Combining System Properties: A Cautionary Example and Formal Examination Combining Theorem Proving and Model Checking through Symbolic Analysis Communication Pattern Anomaly Detection in Process Control Systems A Comparative Analysis Approach for Deriving Failure Scenarios in the Natural Gas Distribution Infrastructure A Comparison of Alternative Audit Sources for Web Server Attack Detection A Comparison of Bus Architectures for Safety-Critical Embedded Systems Complete Proof Systems for First Order Interval Temporal Logic The Complexity and Composability of Secure Interoperation Computer-Aided Computing Computing Abstractions of Infinite State Systems Compositionally and Automatically Congruence Closure Modulo Associativity and Commutativity Construction of abstract state graphs with PVS A context-aware personal desktop assistant Continuity and Synchronization in MPEG Coral - policy language and reasoning techniques for spectrum policies Correct Architecture Refinement Correct Schema Transformations Correct Transformation Rules for Incremental Development of Architecture Hierarchies Correctness and Composition of Software Architectures Correctness of Transformations in High Level Synthesis: Formal Verification Correlated Attack Modeling (CAM) COTS, Integration and Critical Systems Critical System Properties: Survey and Taxonomy Cross-Domain Access Control via PKI Crossing the "Valley of Death": Transitioning Cybersecurity Research into Practice Cryptographic Protocol Generation from CAPSL Cryptography Review of W3C Verifiable Credentials Data Model (VCDM) and Decentralized Identifiers (DIDs) Standards and Cryptography Implementation Recommendations Current Design and Implementation of the Cafe Prover and Knuth-Bendix Checker Tools Cyber Risk Economics Capability Gaps Research Strategy Cyber State Requirements for Design and Validation of Trust in the Critical Transportation Infrastructure Data Cube Indexing of Large-Scale Infosec Repositories Data Security Decision Problems for Propositional Linear Logic Decision Problems in Linear Logic (short form) Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief Decomposing the Proof of Correctness of Pipelined Microprocessors Deconstructing Shostak Demonstration of a Policy Engine For Spectrum Sharing Denial of Service against the Domain Name System Dependability Co-Design Dependability Gauges for Dynamic Systems Depender Graphs: A method of Fault-Tolerant Certificate Distribution Design and Implementation od the Cafe Prover and Church-Rosser Checker Tools Design and Verification of Secure Systems Design Assurance Arguments for Intrusion Tolerance Detecting Anomalies in Cellular Networks Using an Ensemble Method Detecting Computer and Network Misuse Through the Production-Based Expert System Toolset (P-BEST) Detecting Disruptive Routers in Wireless Sensor Networks Detecting Intruders in Computer Systems Detecting Novel Scans Through Pattern Anomaly Detection Detecting Unusual Program Behavior Using the Statistical Components of NIDES The Detection and Elimination of Useless Misses in Multiprocessors Detection, Correlation, and Visualization of Attacks against Critical Infrastructure Systems Disappearing Formal Methods A Duration Calculus Proof Checker Using PVS as a Semantic Framework Dynamic Scan Scheduling Effective Theorem Proving for Hardware Verification An Efficient Decision Procedure for the Theorz of Fixed-Sized Bit-Vectors Efficient Fault-Tolerant Certificate Revocation Effieient Implementation of Lattice Operations Elements of Mathematical Analysis in PVS Elements of Trusted Multicasting Elements of Trusted Multicasting EMERALD: Conceptual Overview Statement EMERALD: Event Monitoring Enabling Responses to Anomalous Live Disturbances Emulation Technology -- Support for Weapon Systems in the 1990's Enclaves: Enabling Secure Collaboration over the Internet Epidemic Profiles and Defense of Scale-Free Networks Execution-Driven Distributed Simulation of Parallel Architectures Experience with EMERALD to Date Experiments in Theorem Proving and Model Checking for Protocol Verification eXpert-BSM: A Host-based Intrusion Detection Solution for Sun Solaris Extending Semantically Enabled Virtual Environments for Training Assessment An Extensible Module Algebra For Maude Fail-Stop Protocols: An Approach to Designing Secure Protocols Fair Synchronous Transition Systems and their Liveness Proofs Fault Tolerance in Parallel Implementations of Functional Languages Fibre channel protocol: Formal specification and verification Finite-State Analysis Of Space Shuttle Contingency Guidence Requirements FME '96 Tutorial: An Introduction to Some Advanced Capabilities of PVS Formal analysis for realtime scheduling Formal Analysis of the Priority Ceiling Protocol A Formal Basis for Structured Multimedia Collaborations Formal Methods and the Certification of Critical Systems Formal Methods and their Role in the Certification of Critical Systems Formal Methods for Dependable Real-Time Systems Formal Methods: Instruments of Justification or Tools for Discovery? Formal Requirements Analysis of an Avionics Control System The Formal Semantics of PVS Formal Specification and Analysis of Active Networks and Communication Protocols: The Maude Experience Formal Specification and Verification for Critical Systems: Tools, Achievements, and Prospects Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems Formal Verification for Fault-Tolerant Architectures: Prolegomena to the design of PVS Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned Formal Verification of Algorithms for Critical Systems The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model Formal Verification of an Avionics Microprocessor Formal Verification of an Interactive Consistency Algorithm for the Draper FTP Architecture Under a Hybrid Fault Model Formal Verification of an Oral Messages Algorithm for Interactive Consistency Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods Formal Verification of the Interactive Convergence Clock Synchronization Algorithm Formal Verification of Transformations on Dependency Graphd in Optimizing Compilers A Formalization of Software Architecture A Formalization of the B-Method in Coq and PVS Formalizing Space Shuttle Software Requirments Formally Specifying Design Goals of Worm Defense Strategies A Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model (1993) A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model (IEEE) The foundations of a provably secure operating system (PSOS) Fractionated Software for Networked Cyber-Physical Systems: Research Directions and Long-Term Vision From Formal Verification to Silicon Compilation From Refutation To Verification From Rewrite Theories to Temporal Logic Theories From VHDL to Efficient and First-Time-Right Designs: A Formal Approach The Future of the Internet of Things Gateway Based Approach for Conducting Multiparty Multimedia Sessions over Heterogeneous Signaling Domaines GEM : An innovative solution to the DMS Problem Generalizing Data to Provide Anonymity when Disclosing Information GLU for Multidimensional Signal Processing GLU Implementation Architectures for Heterogeneous Systems GLU Programmer's Guide Version 0.9 GLU: A High-Level System for Granular Data-Parallel Programming Government-Funded R&D to Drive Cybersecurity Technologies Ground Temporal Logic: A Logic for Hardware Veridication Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study Homogeneity as an Advantage: It Takes a Community to Protect an Application Host Protection Strategies for Industrial Control Systems How to Prove Faithfullness of Elementary Theory Interpretations A Hybrid Quarantine Defense ICS: Integrated Canonizer and Solver IDES: A Progress Report IDES: The Enhanced Prototype Implementing Adaptive Fault-Tolerant Services for Hybrid Faults The Inquisitive Sensor: A Tactical Tool for System Survivability Integrated Formal Verification: Using Model Checking With Automated Abstraction, Invariant Generation, and Theorem Proving Integrating the Unified Modeling Language with an Architecture Description Language Integrating WS1S with PVS Integration in PVS: Tables, Types, and Model Checking Integration In Software Intensive Systems An Integration of Model-Checking with Automated Proof Checking An Integration of Model_Checking with Automated Proof Checking Integration Standards For Critical Software Intensive Sysyems Intelligent Coaching Systems in Higher-Order Applications: Lessons from Automated Content Creation Bottlenecks Intenal Startagies in a Reflective Logic Intensional and Extensional Graphical Models for GLU Programming Internet Security An Introduction to Formal Specification and Verification Using EHDM Introduction to SADL 1.0 A Language for Specifying Software Architecture Hierarchies An Intrusion Detection System for Wireless Process Control Systems Intrusion Monitoring in Process Control Systems Intrusion Tolerant Software Architectures Intrusion-Tolerant Enclaves Intrusion-Tolerant Group Management in Enclaves The Invariant Checker: Automated Deduction Verification of Reactive Systems Inverting the Abstraction Mapping: A Methodology for Hardware Verification InVeSt : A Tool for the Verification of Invariants Kernels for Safety? Key Management and Secure Software Updates in Wireless Process Control Environments A Lazy Approach to Compositional Verification Lazy Compositional Verification Le Fun: Logic, Equations, and Functions A Less Elementary Tutorial for the PVS Specification and Verification System Lightweight Key Management in Wireless Sensor Networks by Leveraging Initial Trust Linear Logic Linearizing Intuitionistic Implication Live Traffic Analysis of TCP/IP Gateways Low-Overhead Time-Triggered Group Membership Machine-Assited Verification Using Theorem Proving and Model Checking Malware Characterization through Alert Pattern Discovery The Maude 2.0 System Maude as a Formal Meta-Tool The Maude LTL Model Checker The Maude LTL Model Checker and Its Implementation The Maude Specification of Full Maude Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis Maude: Specification and Programming in Rewriting Logic Measures and Techniques for Software Quality Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization Mechanical Verification of a Schematic Protocol for Byzantine Fault Tolerant Clock Synchronization Mechanized Formal Methods: Progress and Prospects Mechanized Formal Methods: Where Next? Mechanized Verification of Real-Time Systems Using PVS Mechanizing Formal Methods: Opportunities and Challenges A Meta-notation for Protocol Analysis Microprocessor Verification in PVS Microscopic Simulation of a Group Defense Strategy A Mission-Impact-Based Approach to INFOSEC Alarm Correlation Model Checking and Other Ways of Automating Formal Methods Model Checking Guided Abstraction and Analysis Model Checking of Worm Quarantine and Counter-Quarantine under a Group Defense A Model of Noninterference for Integrating Mixed-Criticality Software Components Model-Based Reconfiguration: Diagnosis and Recovery Model-Based Reconfiguration: Toward an Integration with Diagnosis Modeling Correlated Alarms in Network Management Systems Modeling for E-Service Creation Modeling Group Communication Protocols Using Multiset Term Rewriting Modeling Multistep Cyber Attacks for Scenario Recognition Modeling the Human in Human Factors (Extended Abstract) Models and Mechanized Methods that Integrate Human Factors into Automation Design Modular and Incremental Analysis of Concurrent Software Systems Modular Verification of SRT Division Modular Verification of SRT Division Modular Verification of SRT Division 2 MuCAPSL A Multi-Sensor Model to Improve Automated Attack Detection Multidimensional Problem Solving in Lucid Narrowing Terminates for Encryption A Necessarily Parallel Attack New Protocols for Third-Party_Based Authentication and Secure Broadcast Next Generation Intrusion Detection Expert System (NIDES) The NIDES Statistical Component The NIDES Statistical Component: Description and Justification NIDES: A Summary NIDES: Software Users Manual -- Beta-Update Release NIDES: Training Course -- Beta Release Noninterference, Transitivity, and Channel-Control Security Policies Notification of certificate revocation status between different domains under a PKI system On Location: Points about Regions On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction On Shostack's Decision Procedure for Combinations of Theories On the Feasibility of Deploying Cell Anomaly Detection in Operational Cellular Networks On the Freedom of Decryption Ontological analysis of terrain data Ontologies and tools for analysing and composing simulation confederations for the training and testing domains Ontologies and Tools for Analyzing and Synthesizing LVC Confederations Ontology-based service discovery in p2p networks An Overview of Enclaves 1.0 An Overview of SAL OWL-S Editor The OWL-S editor - a development tool for semantic web services (ESWC) The OWL-S editor - a development tool for semantic web services (YR-SOC) Partitioning in Avionics Architectures: Requirements, Mechanisms, and Assurance The Path of the Blind Watchmaker: A Model of Evolution Pathway Logic: Executable Models of Biological Networks Pathway Logic: Modeling of Protein Functional Domains in Signal Transduction Pathway Logic: Symbolic Analysis of Biological Signaling PBS: Support for the B-Method in PVS PGRIP: PNNI Global Routing Infrastructure Protection PKI and Revocation Survey Plan in Maude: Specifying an Active Network Programming Language A Policy Engine for Spectrum Sharing Policy-based Cognitive Radios Polytypic Proof Construction A Portable Fault-Tolerant Parallel Software MPEG-1 Encoder The Potential to Reduce the DMS Impact on the Space Shuttle Orbiter Powerful Techniques for the Automatic Generalization of Invariants Practical Architectures for Survivable Systems and Networks Principles and Pragmatics of Subtyping in PVS Principles of Maude The Priority Ceiling Protocol: Formalization and Analysis Using PVS Probabilistic Alert Correlation A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm Without a Reorder Buffer Proof of Correctness of a Processor with Reorder Buffer using the Completion Functions Approach Proof Search in First-order Linear Logic and other Cut-free Sequent Calculi Proof Search in the Intuitionistic Sequent Calculus Proof Synthesis via Explicit Substitutions on Open Terms Protecting Collaboration (Proceedings of the 1996 AMIA Conference) Protecting Inappropriate Release of Data from Realistic Databases Protecting Privacy when Disclosing Information: k-Anonymity and its Enforcement through Generalization and Suppression Protocol Specification and Analysis in Maude Protocol-Independent Secrecy Provably Dependable Software Architectures Provably Dependable Software Architectures For Adaptable Avionics Proving Secrecy is Easy Enough Purpose-Aware Interoperability: The ONISTT Ontologies and Analyzer Purpose-aware reasoning about interoperability of heterogeneous training systems PVS Bibliography The PVS Proof Checker: A Reference Manual (Beta Release) The PVS Specification Language (Beta Release) PVS: A Prototype Verification System PVS: An Experience Report PVS: Combining Specification, Proof Checking and Model Checking PVS: Combining Specification, Proof Checking, and Model Checking Quality Measures and Assurance for AI Software Quantitative Fault Propagation Analysis for Networked Cyber-Physical Systems Query Folding Query Mediation for Trusted Database Interoperation Rank Analysis in the GLU Compiler Reachability Verification for Hybrid Automata A REAL-TIME INTRUSION DETECTION EXPERT SYSTEM (IDES) Reasoning about resources and hierarchical tasks using OWL and SWRL Reasoning About Trust and Insurance in a Public Key Infrastructure Reconfiguration and Transient Recovery in State-Machine Architectures Reflection and Strategies in Rewriting Logic Reflection in Rewriting Logic and its Applications in the Maude Language A Reflective Module Algebra with Applications to the Maude Language Relating Strands and Multiset Rewriting for Security Protocol Analysis (Revised Extended Abstract) Representing, Verifying and Applying Software Development Steps using the PVS System Requirements Analysis of Real-Time Control Systems using PVS Results on Event-Recording Logic The Rewrite Rule Machine Node Architecture and its Performmance Rewriting Logic as a Semantic Framework for Concurrency: a Progree Report Rewriting Semantics of Meta-Objects and Composable Distributed Services Rigid E-Unification Revisited The Risks of Key Recovery, Key Escrow, and Trusted Third-Party Encryption Robust Nonproprietary Software Scan Scheduling Specification and Analysis SDTP---A Multilevel-Secure Distributed Transaction Processing System Secure Auction in a Publish/Subscribe System Secure Interoperation of Heterogeneous Systems: A Mediator-Based Approach Secure Interoperation of Secure Distributed Databases: An Architecture Verification Case Study Secure Software Architectures Securing Collaborative Intrusion Detection Systems Securing Control Systems in the Oil and Gas Infrastructure Securing Current and Future Process Control Systems Securing the Software-Defined Network Control Layer Security Issues in Data Warehousing and Data Mining: Panel Discussion Security Requirements Specifications: How and What? Self-Checking Prover Study Final Report Semantic Instrumentation of Virtual Environments for Training Semantic Interoperation: A Query Mediation Approach A semantic web reasoner for rules, equations and constraints Semantical Investigations of Linear Logic Semantics-Preserving Message Translation Sensor Coordination Using Active Dataspaces Sensor Data Dissemination through Ad Hoc Battlefield Communications Service Configuration and Management in Adaptable Networks A Simplified Method for Establishing the Correctness of Architectural Refinements Size Format SAFEGUARD Final Report: Detecting Unusual Program Behavior Using the NIDES Statistical Component Software Requirements Specification: Next-Generation Intrusion Detection Expert System Solving Bit-Vector Equations Some Theorems We Should Prove Specification and Verification od the Real-Time Part of a Steam Boiler Control System Specification, Proof Checking, and Model Checking for Protocols and Distributed Systems with PVS Specifying a Reliable Broadcasting Protocol in Maude The SRI IDES Statistical Anomaly Detector SRI International Work on Cybereconomic Incentives for the Department of Homeland Security Science and Technology Directorate Cyber Security Division SRI-CSL Technical Report: Execution-driven Distributed Simulation of Parallel Architectures State Transition Analysis: A Rule-Based Intrusion Detection Approach StegoTorus: A Camouflage Proxy for the Tor Anonymity System Steps Towards Mechanizing Program Transformations Using PVS Stochastic Assembly of Sublithographic Nanoscale Interfaces Structured Theories and Institutions Sublithographic semiconductor computing systems Subtypes for Specifications Subtypes for Specifications: Predicate Subtyping in PVS Survivability Measure SWRL-IQ: A Prolog-based Query Tool for OWL and SWRL Symbolic Analysis of Transition Systems Symbolic Protocol Analysis with Products and Diffie-Hellman Exponentiation SYSTEM DESIGN DOCUMENT: NEXT-GENERATION INTRUSION DETECTION EXPERT SYSTEM (NIDES) Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms (1997) Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms (1999) Systematic Formal Verification of Interpreters TCP SYN Flooding Defense A Technique for Invariant Generation A Technique for the Distributed Simulation of Parallel Computers Tempo: A Model Checker for Event-Recording Automata Theorem Proving for Verification Theorem Proving: Not an Esoteric Diversion, but the Unifying Framework for Industrial Verification A Tool for Proving Invariance Properties of Concurrent Systems Automatically Toward a Scalably Efficient Parallel Implementation of a Hybrid Intensional Language Toward Findable, Accessible, Interoperable, and Reusable Cybersecurity Artifacts Towards automatic synthesis of security protocols Towards Light-Weight Verication and Heavy-Weight Testing Transformations in High-Level Synthesis: Formal Specification and Efficient Mechanical Verification A Tutorial Introduction to PVS A Tutorial on Specification and Verification Using PVS (Beta Release) A Tutorial on Using PVS for Hardware Verification Twords a Duration Calculus Proof Assitant in PVS Ubiquitous Abstraction: A New Approach for Mechanized Formal Verification (Extended Abstract) Unifying Verification Paradigms (Extended Abstract) The Use of White Holes to Mislead and Defeat Importance Scanning Worm User Guide for the PVS Specification and Verification System (Beta Release) Using a PVS Embedding of CSP to Verify Authentication Protocols Using model checking to help discover mode confusions and other automation surprises Using Model-based Intrusion Detection for SCADA Networks Using PVS in Batch Mode Using PVS to Prove a Z Refinement: A Case Study Using PVS to Prove Some Theorems of David Parnas Validation and Testing of Knowledge-Based Systems: How Bad Can It Get? Varifying Invariants Using Theorem Proving VEIL - A System for Certifying Video Provenance Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis Verification of Real-Time Systems Using PVS Verifying a Self-Stabilizing Mutual Exclusion Algorithm View-Based Access Control with High Assurance Web Implementation of a Security Mediator for Medical Databases Workshop Report: Paving the Road to Future Automotive Research Datasets: Challenges and Opportunities

About Us    R&D Divisions    Careers    Newsroom    Contact Us
© 2025 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy