Downloadable papers

  • composition/

  • Model Checking and Modular Verification
  • Liveness in Timed and Untimed Systems
  • Reactive Modules
  • An Inheritance-Based Technique for Building Simulation Proofs Incrementally
  • Composition: A Way to make proofs harder
  • Composing Specifications
  • Conjoining Specifications
  • Automating First-Order Relational Logic
  • alloy: A Lightweight Object Modelling Notation
  • A Formal Model for Dynamic Computation
  • Dynamic Input/Output Automata: a Formal Model for Dynamic Systems


    hybrid/

  • A Toolbox for Proving and Maintaining Hybrid Specifications
  • The Algorithmic Analysis of Hybrid Systems
  • Hybrid I/O Automata Revisited
  • From Timed to Hybrid Systems
  • Deductive verification of hybrid systems using STeP
  • Verification of Clocked and Hybrid Systems
  • Verifying Clocked Transition Systems


    liveness/

  • Liveness Preserving Simulation Relations
  • A Verification Environment for I/O Automata Based on Formalized Meta-Theory
  • Alternating Automata: Checking Truth and Validity for Temporal Logics


    probability/

  • SPNP: Stochastic Petri Net Package
  • Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: A Case Study


    safety/

  • Computational Processes
  • Proof Methods for State Machines
  • Composing and Decomposing Computational Processes
  • Model Checking and Abstraction
  • Verification Tools of Finite State Concurrent Systems
  • An Introduction to Input/Output Automata
  • Symmetry and Model Checking
  • Dynamically Discovering Likely Program Invariants to Support Program Evolution
  • Forward and Backward Simulations Part I: Untimed Systems
  • Abstraction Based Verification of Distributed Systems
  • Specifying Concurrent Systems with TLA+
  • The Temporal Logic of Actions
  • Temporal Verification Diagrams
  • Using I/O Automata for Developing Distributed Systems
  • IOA: A Language for Specifying, Programming and Validating Distributed Systems
  • Model Checking
  • Automatic Verification of Finite State concurrent Systems Using Temporal Logic Specifications
  • On Visual Formalisms
  • PVS: Comgining Specification, Proof Checking, and Model Checking
  • PVS Language Reference
  • PVS Prover Guide
  • PVS System Guide


    timed/

  • Modularity for Timed and Hybrid Systems
  • Forward and Backward Simulations Part II: Timing-Based systems
  • A Theory of Timed Automata
  • Timed Automata
  • Automatic Symbolic Verification of Embedded Systems
  • Model checking timed automata