CS 525: Formal Methods for System Verification

Instructor

• Dr. Chandan Karfa

Class Timing and Venue:

• Slot A1 in timetable for Electives

• Monday: 5PM-6PM, Tuesday: 4PM-5PM, Wednesday: 3PM-4PM

• Venue: 5G1, Core 5

Teaching Assistants

• Praveen Karmakar - pkarmakar@iitg.ac.in

• Nilotpola Sarma - s.nilotpola@iitg.ac.in

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.

• SAT Solver

• SMT Solver

• 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.

Text Books

• [Manna] Aaron R. Bradley, Zohar Manna: The Calcular of Computation, Springer 2010.

• [Kroening] Daniel Kroening and Ofer Strichman: Decision Procedures - An Algorithmic Point of View, Springer, 2008

• [Huth] M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Ed, Cambridge University Press, 2004.

• [PDG] Pallab Dasgupta, A Roadmap for Formal Property Verification, Springer, 2006.

• [Katoen] Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, May 2008.

• Various Research Papers.

Grade Calculation

• Quiz: 10%

• MidSem: 30%

• End Sem: 40%

• Project: 20%. A group of 4/5 students to be assigned to a project.

Classes

Project Presentation Schedule

Evaluation Schedule