Advanced Topics in Software Systems  (Formal Methods for Reactive Systems)

Main Textbook:

Alur R. and Henzinger T.A., “Computer Aided Verification,” Draft, 1999.

Other Textbooks:

Manna Z. and Pnueli A., “The Temporal Logic of Reactive and
 Concurrent Systems: Specification,” Springer-Verlag New York,  Inc., 1992.

Clarke E.M., Grumberg O., and Peled D.A., “Model Checking,” MIT Press, 1999.


The course introduces the theory and practice of formal methods for the design and analysis of concurrent and reactive 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