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.

 Topics:

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

Syllabus