Computer-Aided Verification

© Rajeev Alur and Thomas A. Henzinger

• Prerequisite Notions and Notations (Postscript, PDF)
• Reactive Modules (Postscript, PDF)
  • Definition of reactive modules
    • Variables
    • Atoms
    • Modules
  • Operations on reactive modules
    • Parallel composition
    • Variable renaming
    • Variable hiding
  • Examples of reactive modules
    • Synchronous circuits
    • Shared-variables protocols
    • Message-passing protocols
    • Asynchronous circuits
• Invariant Verification (Postscript, PDF)
  • Transition graphs
    • Definition of transition graphs
    • From reactive modules to transition graphs
    • The reachability problem
  • Invariants
    • The invariant-verification problem
    • From invariant verification to reachability
    • Monitors
  • Graph traversal
    • Reachability checking
    • Enumerative graph and region representations
    • Invariant verification
    • Three space optimizations
  • State explosion
    • Hardness of invariant verification
    • Complexity of invariant verification
  • Compositional reasoning
    • Composing invariants
    • Assuming invariants