Menu

CS 525: Formal Methods for System Verification

Course Feedback:

overal Feedback 
Comments for Instructor 
Announcements:

  • Welcome to CS 525 Course page

  • The Class will strat from 9th Januaray 2025 (Friday) in 5G2.

  • Attendance is Mandetory in the Course.

  • IMPORTANT: Any malpractice will lead to F grade without any explanation.

Instructor

  • Dr. Chandan Karfa

Class Timing and Venue:

  • Slot G in timetable for Electives

  • Wednesday: 12Pm to 1PM, Thursday: 12Pm to 1PM, Friday: 12Pm to 1PM,

  • Venue: 5G2, Core 5

Teaching Assistants

  • Bhabesh Mali - m.bhabesh@iitg.ac.in

  • E. B. Eswar Reddy - r.eddula@iitg.ac.in

  • Tapish Patidar - p.tapish@iitg.ac.in

Syllabus

  • Pre-requisites: (1) Basic knowledge of FLAT

  • 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 and Class Participation: 20%

  • MidSem: 20%

  • End Sem: 40%

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

Classes

Lecture No Date Topic Resources
1. 8th Jan 2026 Course Introduction Class notes
2. 15th Jan 2026 Formal Methods with Example Class notes
3. 16th Jan 2026 Spectrum as Logic Class notes
4. 21st Jan 2026 Propositional Logic Class Notes, Manna - Ch 1
5. 22nd Jan 2026 Propositional Logic: Deduction Method Class Notes, Manna - Ch 1
6. 23rd Jan 2026 Propositional Logic: Normal Forms Class Notes, Kroening - Ch 1
7. 28th Jan 2026 Propositional Logic: Tseitin Transformation Class Notes, Kroening - Ch 1
8. 29th Jan 2026 Introduction to SAT Solver; Binary Resolution Class Notes, Kroening - Ch 2
9. 2nd Feb 2026 SAT Solver: DPLL; Unit Clause Resolution Class Notes, Kroening - Ch 2
10. 4th Feb 2026 SAT Solver: Implication Graph; Conflict Clause Class Notes, Kroening - Ch 2
11. 11th Feb 2026 UIP; Analyze Conflict Class Notes, Kroening - Ch 2
12. 12th Feb 2026 SAT Solver: Analyze Conflict; Corrections Class Notes, Kroening - Ch 2
13. 13th Feb 2026 Decision Heuristics Class Notes, Kroening - Ch 2
14. 16th Feb 2026 Preprocessing of SAT Formula Class Notes, Kroening - Ch 2
15. 18th Feb 2026 Class Test 1 Question paper
16. 19th Feb 2026 ROBDD & Variable Ordering Class Notes, Kroening - Ch 2
17. 20th Feb 2026 ROBDD Construction (Direct Method) Class Notes, Kroening - Ch 2
18. 24th Feb 2026 Formal Property Checking: Introduction Class Notes, PDG: Ch 1
19. 25th Feb 2026 Correctness, Consistency & Completeness Properties Class Notes, PDG: Ch 1
20. 26th Feb 2026 Property Checking Approach Class Notes, PDG: Ch 1
21. 09th Mar 2026 LTL Model Checking Class Notes, Huth: Ch 3
22. 18th Mar 2026 LTL Properties, CTL Basics Class Notes, Huth: Ch 3
23. 19th Mar 2026 CTL Operators and Semantics Class Notes, Huth: Ch 3
24. 20th Mar 2026 CTL Property Examples Class Notes, Huth: Ch 3
25. 01st Apr 2026 CTL Model Checking Algorithm Class Notes, Huth: Ch 3
26. 06th Apr 2026 Büchi Automata and LTL Class Notes, Katoen: Ch 5
27. 08th Apr 2026 LTL Model Checking Algorithm Class Notes, Katoen: Ch 5
28. 10th Apr 2026 CNF Construction from LTL Formulae Class Notes, Katoen: Ch 5
29. 16th Apr 2026 Quiz 2 -
30. 17th Apr 2026 LTL Model Checking Class Notes, Katoen: Ch 5
31. 18th Apr 2026 Symbolic Model Checking with BDD Class Notes, PDG: Ch 3
32. 20th Apr 2026 Symbolic Model Checking with BDD (Contd.) Class Notes, PDG: Ch 3
33. 22nd Apr 2026 SAT-Based Model Checking (Introduction) Class Notes, PDG: Ch 4
34. 23rd Apr 2026 SAT-Based Model Checking Class Notes, PDG: Ch 4
35. 25th Apr 2026 Bounded Model Checking Class Notes, PDG: Ch 4
36. 27th Apr 2026 Project Evaluation -
37. 29th Apr 2026 Project Evaluation -
38. 28th Apr 2026 Equivalence Checking Class Notes, PDG: Ch 5

Project Presentation Schedule (Last Year)

Date Time Groups
4th Nov 2024 6:30PM to 8:30PM A1, A4, A5, A6
5th Nov 2024 5:30PM to 7:30PM A7, A8, A10, C2
7th Nov 2024 4PM to 6:30PM B1, B2, B3, B9
8th Nov 2024 4PM to 7PM B8, B10, C3, C4, B5, B4, B6
9th Nov 2024 10AM to 1PM C6, C7, C8, C9, C10, A2, A9, B7
11th Nov 2024 6:15PM to 8:30PM C1, C5, A3, A11

Evaluation Schedule