CS 525, Formal Methods for System Verification
Purandar Bhaduri, ext: 2360, email: pbhaduri.
Course Contents (Tentative)
Introduction to Formal Methods
Review of Propositional Logic and Predicate Logic
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.
Some Useful Links
1. Course on Bug Catching: Automated Program Verification and Testing at CMU.
2. Course on Introduction to Model Checking at CMU.
3. 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,
5. 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. Download and install NuSMV from the above website, and learn how to use it.
2. Describe the protocol and its important properties in NuSMV. Specify as many properties as you can.
3. Verify the model using the NuSMV model checker.
4. Submit a report (maximum length 5 pages) describing the model and the properties specified and verified. You should discuss important decisions and simplifications made, along with the limitations of SMV (if any) in the modelling exercise.
5. Submit the SMV model and the results of verification.
Deadline: 3 November, 2006 (Friday). News: The deadline has been extended to 6 November, 2006 (Monday) 6 PM.
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.