CS 525, Formal Methods
for System Verification
Spring 2008 - 2009Instructor 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 Prerequisites CS203 (Discrete Maths), CS301 (Formal Languages and Automata Theory) Textbook M. Huth and M. Ryan, Logic in
Computer Science: Modelling and Reasoning about Systems,
Second 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. Evaluation 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, 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 Homeworks 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.
|
|
|