CSE 625: Computer Aided Verification, Spring 2003

(Listed as Asynchronous Systems)


Instructor: Radu Grosu ( grosu@cs.sunysb.edu),

Class: TueThu  2:20pm - 3:40pm, Melville Library room N4006

Office hours: TueThu 4-5pm, CS Building room 1425, and by appointment


Reactive systems are becoming an integral part of nearly every engineered product: they control consumer products, commercial aircraft, nuclear power plants, medical devices, weapon systems, aerospace systems, automobiles, public transportation systems, and so on.  At the same time quality and confidence issues are increasing in importance. Errors may result in loss of life, destruction of property, failure of businesses, and environmental harm.  Today, designers check that a reactive system works properly by using simulation and testing. However, as reactive systems become more complex and pervasive, these traditional techniques are not sufficient to assure desired reliability. Model checking and related computer-aided verification techniques are emerging as practical alternatives. They allow the designer to verify that a mathematical model of a system satisfies its abstract logical specification. This approach has been most effective for control-intensive components, and is rapidly becoming an integral part of the design cycle in many companies.


The participants will learn how to model a reactive (hardware or software) sytem, express desired properties of the reactive system and check that the system satisfies these properties. They will get familiar with  the algorithmic methods used for this check.


The course requires basic knowledge of algorithms, data structures, automata theory, computational complexity, and propositional logic. Knowledge of operating systems, communication protocols, and hardware is useful. The course requires mathematical maturity, and is appropriate for graduate students who wish to pursue research in formal methods or related areas. If you need more information to decide, contact the instructor.


The course introduces the theory and practice of formal methods for the design and analysis of concurrent and embedded systems. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity. Topics include


We will use the model checker MOCHA being currently developed at Stony Brook, UPenn and UC Berkeley.

Related tools include


The course will use the draft of a forthcoming textbook titled Computer-aided verification by R. Alur & T. Henzinger. Chapters will be posted on the web as needed. Following books are recommended for additional reading


There will be periodic homework assignments consisting of problems and experimentation with MOCHA.

 There will be no exams.

 There will be a class project. The project can be done in groups of two or three, and will require a presentation in the final week. Projects can be of various forms:

Tentative Schedule

0 Introduction
  • 1/25:Introduction

  • 1 Modeling Lanuage Reactive Modules
  • 1/28, 1/30: Definition, operations on reactive modules, examples

  • 2 Invariant verification
  • 2/4,6: Transition graphs, invariants, graph traversal, state explosion, compositional reasoning

  • 3 Symbolic Graph Search
  • 2/11,13: Symbolic invariant verification,  binary decision diagrams BDDs

  • 4 Graph Minimization
  • 2/18,20: Graph partitions, partition refinement, reachable partition refinement

  • 5 Temporal Safety Requirements
  • 2/25: State logics, safe temporal logic STL
  • 2/27: STL model checking, distinguishing and expressive power

  • 6 Automata-theoretic Safety Verification
  • 3/4: Automata, safe automata logic SAL, operations on automata, model checking7: Hierarchical Verification

  • 7 Hierarchical Verification
  • 3/6: Trace semantics, compositionality, asssume-guarantee
  • 3/11: Simulation relations, homomorphisms

  • 8 Fair Modules
  • 3/13: Omega-languages, safety versus liveness
  • 3/25: Fairness, fair modules, examples

  • 9 Response Verification
  • 3/27: Searching for fair cycles and response verification

  • 10 Temporal Liveness Requirements
  • 4/1: CTL, Mu-calculus, and Symbolic model checking

  • 11 Automata-theoretic Liveness Verification
  • 4/3: Theory of omega-regular languages

  • 12 Linear Temporal Logic
  • 4/8: Linear temporal logic LTL

  • 4/10,15: MSCs, hierarchical modules, and UML
    Week of 5/1: Project presentations

    Last updated on Feb 4, 2003 by Radu Grosu