CS 525, Formal Methods for System Verification
Spring 2008 - 2009
Purandar Bhaduri, ext: 2360, email: pbhaduri
Praveen Moparthy (email: p.moparthy)
Ramanuj Chouksey (email: ramanuj)
Introduction to Formal Methods
Verification by Model Checking: LTL, CTL and CTL*
Binary Decision Diagrams and Symbolic Model Checking
CS203 (Discrete Maths), CS301 (Formal Languages and Automata Theory)
M. Huth and M. Ryan, Logic in
Computer Science: Modelling and Reasoning about Systems,
Model Checking, Edmund M. Clarke, Orna Grumberg and Doron A. Peled, MIT Press, January 2000.
Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, May 2008.
Some Useful Links
1. Course on Bug Catching: Automated Program Verification and Testing at CMU.
2. Course on Introduction to Model Checking at CMU.
1. Tutorial on SAT Beyond Propositional Satisfiability by Roberto Sebastiani in CADE 2003.
Temporal Logic and Büchi Automata Tutorial talk by Madhavan Mukund, Winter School on Logic and Computer
Science, Indian Statistical Institute,
3. Finite-state Automata on Infinite Inputs, Tutorial talk by Madhavan Mukund, Sixth National Seminar on Theoretical Computer Science, Banasthali Vidyapith, Banasthali, Rajasthan, August 1996.
Tools for Finite-State Concurrent Systems, Edmund M. Clarke, Orna
Grumberg and David E. Long in REX '93
School/ Workshop: 'A Decade of Concurrency'. Noordwijkerhout, The
1. Homework Problem. Due date: 13 April, Monday. Submit to the TAs.
No late submissions will be accepted! The work must be done on your own. Two or more identical or near identical solutions will get zero credit.