|
Chandan Karfa
CS 525: Formal Methods for System Verification
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
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
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
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 |
|
|
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
|