CS 525, Formal Methods for System Verification

 Spring 2008 - 2009


Purandar Bhaduri, ext: 2360, email: pbhaduri

Teaching Assistants

Praveen Moparthy (email: p.moparthy)

Ramanuj Chouksey (email: ramanuj)

Course Contents

Introduction to Formal Methods

Verification by Model Checking: LTL, CTL and CTL*

Binary Decision Diagrams and Symbolic Model Checking

Program Verification


CS203 (Discrete Maths), CS301 (Formal Languages and Automata Theory)


M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Second Edition, Cambridge University Press, 2004. (Available in South Asian edition)


Reference Book

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.



Assignments    15%

Midsem            35%

Endsem            50%



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.

2.       Linear-Time Temporal Logic and Büchi Automata Tutorial talk by Madhavan Mukund, Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, January 1997.  (Please read Sections 1 – 3).

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.

4.       Verification 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 Netherlands, June 1-4, 1993. Springer Lecture Notes in Computer Science, No. 684, pp. 124-175, 1994.


1.      Homework Problem. Due date: 13 April, Monday. Submit to the TAs.

Homework Policy

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.

 back to homepage