    

Papers
 20 Years of Covert Channel Modeling and Analysis
 31st Annual Simulation Symposium: Highfidelity 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 MonteCarlo Method for the Analysis of
 An Abstract MonteCarlo 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 DAMLEnabled Web
 An Adaptable Network COntrol and Reporting System (ANCORS)
 Adaptive FaultResistant Systems
 Adaptive, Modelbased Monitoring for Cyber Attack Detection
 Analyzing Cockpit Interfaces Using Formal Methods
 Analyzing Tabular and StateTransition Specifications in PVS
 ANCORS: Adaptable Network Control and Reporting Systems
 Application Experience with an Implicitly Parallel Composition Language
 ApplicationIntegrated 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
 An Approach to Sensor Correlation
 Architectural Support for Copy and Tamper Resistant Software
 An Architecture for an Adaptive Intrusion Tolerant Server
 ArchitectureDriven Software Component Retrieval
 Architectures and Formal Representations for Secure Systems
 AssociativeCommutative 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
 Axiomatizing Reflective Logics and Languages
 Bonsai: Balanced Lineage Authentication
 Bounded Model Checking for Timed Automata
 Building Equational Proving Tools by Reflection in Rewriting Logic
 Bus Architectures For SafetyCritical 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)
 The CAPSL Integrated Protocol Environment
 CAPSL Interface for the NRL Protocol Analyzer
 CAPSL Intermediate Language
 A CaseStudy in ComponentBased Mechanical Verification of FaultTolerant 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 ProofCarrying 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 runtime 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 Comparison of Alternative Audit Sources for Web Server Attack Detection
 A Comparison of Bus Architectures for SafetyCritical Embedded Systems
 Complete Proof Systems for First Order Interval Temporal Logic
 The Complexity and Composability of Secure Interoperation
 ComputerAided Computing
 Computing Abstractions of Infinite State Systems Compositionally and Automatically
 Congruence Closure Modulo Associativity and Commutativity
 Construction of abstract state graphs with PVS
 A contextaware 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
 CrossDomain Access Control via PKI
 Crossing the "Valley of Death": Transitioning Cybersecurity Research into Practice
 Cryptographic Protocol Generation from CAPSL
 Current Design and Implementation of the Cafe Prover and KnuthBendix Checker Tools
 Data Cube Indexing of LargeScale 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 CoDesign
 Dependability Gauges for Dynamic Systems
 Depender Graphs: A method of FaultTolerant Certificate Distribution
 Design and Implementation od the Cafe Prover and ChurchRosser 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 ProductionBased Expert System Toolset (PBEST)
 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 FixedSized BitVectors
 Efficient FaultTolerant 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 ScaleFree Networks
 ExecutionDriven Distributed Simulation of Parallel Architectures
 Experience with EMERALD to Date
 Experiments in Theorem Proving and Model Checking for Protocol Verification
 eXpertBSM: A Hostbased Intrusion Detection Solution for Sun Solaris
 An Extensible Module Algebra For Maude
 FailStop 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
 FiniteState 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 RealTime 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 FaultMasking and TransientRecovery Model for Digital FlightControl Systems
 Formal Verification for FaultTolerant Architectures: Prolegomena to the Design of PVS
 Formal Verification for FaultTolerant 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 SCRStyle 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 BMethod 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 CyberPhysical Systems: Research Directions and LongTerm Vision
 From Formal Verification to Silicon Compilation
 From Refutation To Verification
 From Rewrite Theories to Temporal Logic Theories
 From VHDL to Efficient and FirstTimeRight Designs: A Formal Approach
 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 HighLevel System for Granular DataParallel Programming
 Ground Temporal Logic: A Logic for Hardware Veridication
 Hierarchical Verification of TwoDimensional HighSpeed 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 FaultTolerant 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 ModelChecking with Automated Proof Checking
 An Integration of Model_Checking with Automated Proof Checking
 Integration Standards For Critical Software Intensive Sysyems
 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
 IntrusionTolerant Enclaves
 IntrusionTolerant 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
 LowOverhead TimeTriggered Group Membership
 MachineAssited Verification Using Theorem Proving and Model Checking
 Malware Characterization through Alert Pattern Discovery
 The Maude 2.0 System
 Maude as a Formal MetaTool
 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 RealTime Systems Using PVS
 Mechanizing Formal Methods: Opportunities and Challenges
 A Metanotation for Protocol Analysis
 Microprocessor Verification in PVS
 Microscopic Simulation of a Group Defense Strategy
 A MissionImpactBased 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 CounterQuarantine under a Group Defense
 A Model of Noninterference for Integrating MixedCriticality Software Components
 ModelBased Reconfiguration: Diagnosis and Recovery
 ModelBased Reconfiguration: Toward an Integration with Diagnosis
 Modeling Correlated Alarms in Network Management Systems
 Modeling for EService 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 MultiSensor Model to Improve Automated Attack Detection
 Multidimensional Problem Solving in Lucid
 Narrowing Terminates for Encryption
 A Necessarily Parallel Attack
 New Protocols for ThirdParty_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  BetaUpdate Release
 NIDES: Training Course  Beta Release
 Noninterference, Transitivity, and ChannelControl 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 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
 Ontologybased service discovery in p2p networks
 Optimizing Protocol Rewrite Rules of CIL Specifications
 An Overview of Enclaves 1.0
 An Overview of SAL
 OWLS Editor
 The OWLS editor  a development tool for semantic web services (ESWC)
 The OWLS editor  a development tool for semantic web services (YRSOC)
 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 BMethod 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
 Policybased Cognitive Radios
 Polytypic Proof Construction
 A Portable FaultTolerant Parallel Software MPEG1 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 Firstorder Linear Logic and other Cutfree 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: kAnonymity and its Enforcement through Generalization and Suppression
 Protocol Specification and Analysis in Maude
 ProtocolIndependent Secrecy
 Provably Dependable Software Architectures
 Provably Dependable Software Architectures For Adaptable Avionics
 Proving Secrecy is Easy Enough
 PurposeAware Interoperability: The ONISTT Ontologies and Analyzer
 Purposeaware 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 CyberPhysical Systems
 Query Folding
 Query Mediation for Trusted Database Interoperation
 Rank Analysis in the GLU Compiler
 Reachability Verification for Hybrid Automata
 A REALTIME 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 StateMachine 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 RealTime Control Systems using PVS
 Results on EventRecording Logic
 The Rewrite Rule Machine Node Architecture and its Performmance
 Rewriting Logic as a Semantic Framework for Concurrency: a Progree Report
 Rewriting Semantics of MetaObjects and Composable Distributed Services
 Rigid EUnification Revisited
 The Risks of Key Recovery, Key Escrow, and Trusted ThirdParty Encryption
 Robust Nonproprietary Software
 Scan Scheduling Specification and Analysis
 SDTPA MultilevelSecure Distributed Transaction Processing System
 Secure Auction in a Publish/Subscribe System
 Secure Interoperation of Heterogeneous Systems: A MediatorBased 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
 Security Issues in Data Warehousing and Data Mining: Panel Discussion
 Security Requirements Specifications: How and What?
 SelfChecking Prover Study Final Report
 Semantic Interoperation: A Query Mediation Approach
 A semantic web reasoner for rules, equations and constraints
 Semantical Investigations of Linear Logic
 SemanticsPreserving 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: NextGeneration Intrusion Detection Expert System
 Solving BitVector Equations
 Some Theorems We Should Prove
 Specification and Verification od the RealTime 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
 SRICSL Technical Report: Executiondriven Distributed Simulation of Parallel Architectures
 State Transition Analysis: A RuleBased 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
 SWRLIQ: A Prologbased Query Tool for OWL and SWRL
 Symbolic Analysis of Transition Systems
 Symbolic Protocol Analysis with Products and DiffieHellman Exponentiation
 SYSTEM DESIGN DOCUMENT: NEXTGENERATION INTRUSION DETECTION EXPERT SYSTEM (NIDES)
 Systematic Formal Verification for FaultTolerant TimeTriggered Algorithms (1997)
 Systematic Formal Verification for FaultTolerant TimeTriggered 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 EventRecording 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
 Towards automatic synthesis of security protocols
 Towards LightWeight Verication and HeavyWeight Testing
 Transformations in HighLevel 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 Modelbased 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 KnowledgeBased 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 InfiniteState Systems by Combining Abstraction and Reachability Analysis
 Verification of RealTime Systems Using PVS
 Verifying a SelfStabilizing Mutual Exclusion Algorithm
 ViewBased Access Control with High Assurance
 Web Implementation of a Security Mediator for Medical Databases


