| Course Code: CS525 Course Name: Formal Methods For System Verification Prerequisites: NIL Syllabus: Introduction to formal methods and hardware verification. Review of logics: Propositional Calculus and Predicate Calculus. Axioms and rules of Floyd-Hoare Logic. Application of Floyd-Hoare logic to verify hardware circuits. Describing hardware directly in higher order logic. Combinational and sequential behaviour of circuits. Specification of hardware systems. Introduction to Binary Decision Diagram (BDD) and modelling hardware with BDDs. Algorithms for BDD operations. Concept of OBDDs and ROBDDs and operation on ROBDDs. Introduction to Temporal Logic. Linear and Branching time temporal logic. Expressing properties in CTL and CTL*. CTL model checking algorithm. State space explosion problem: Symbolic data structure and symbolic model checking algorithms. Concept of on-the-fly model checking and automata-theoretic model checking. Study of verification tools: SMV and PVS. References: 1. M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Ed, Cambridge University Press, 2004. 2. T. F. Melham, Higher Order Logic and Hardware Verification, Cambridge University Press, 1993. 3. E. M. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999. 4. K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publisher, 1993. 5. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent System Specification, Springer-Verlag, 1992. |