CS 525: Formal Methods for System Verification
Overall Course Feedback:
 |
 |
 |
Welcome to CS 525 Course page
The Class will strat from 31st July 2023 (Monday) in L1.
IMPORTANT: Any malpractice will lead to F grade without any explanation.
Instructor
Dr. Chandan Karfa
Class Timing and Venue:
Slot A1 in timetable for Electives
Monday: 5PM-6PM, Tuesday: 4PM-5PM, Wednesday: 3PM-4PM
Venue: L1, Lecture Hall Complex
Mode of Lecture: Live Class
Teaching Assistants
Praveen Karmakar - pkarmakar@iitg.ac.in
Nilotpola Sarma - s.nilotpola@iitg.ac.in
Akash Lal Dutta - d.akash@iitg.ac.in
Anuj Singh Thakur - anuj.thakur@iitg.ac.in
Vaishali Chaudhari - c.vaishali@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
| Lecture No | Date | Topic | Resources |
| 1. | 31st July 2023 | Course Introduction | Class notes |
| 2. | 1st August 2023 | Formal Modelling with Examples: Eq of Programs, Eq of Ckts, Seq Ckt, Logistic problem | Class Notes |
| 3. | 2nd August 2023 | Introduction of Propostional, First Order and Second Order Logic with Examples | Class Notes |
| 4. | 7th August 2023 | Well Formed Formulas - Formalization | Class Notes |
| 5. | 8th August 2023 | Propositional Logic, NNF, DNF | Class Notes, Kroening - Ch 2 |
| 6. | 9th August 2023 | Propositional Logic: CNF, Tseitin Encoding | Class Notes, Kroening - Ch 2 |
| 7. | 14th August 2023 | Propositional Logic: Tseitin Encoding Optimizations | Class Notes, Kroening - Ch 2 |
| 8. | 16th August 2023 | SAT Solving: Resolution, Unit Clause resolution | Class Notes, Kroening - Ch 2 |
| 9. | 17th August 2023 | SAT Solving: DPLL, Conflict Clause, Implication Graph | Class Notes, Kroening - Ch 2 |
| 10. | 21st August 2023 | SAT Solving: Asserting Clause, Backtrack, Analyze clause | Class Notes, Kroening - Ch 2 |
| 11. | 22nd August 2023 | SAT Solving: Decision Heuristics, DIMACS format | Class Notes, Kroening - Ch 2 |
| 12. | 23rd August 2023 | BDD, ROBDD | Class Notes, Kroening - Ch 2 |
| 13. | 28th August 2023 | Direct ROBDD construction | Class Notes, Kroening - Ch 2 |
| 14. | 29th August 2023 | Variable Ordering, ITE, Modelling example with BDD | Class Notes, Kroening - Ch 2 |
| 15. | 30th August 2023 | Quiz 1 | |
| 16. | 4th September 2023 | Formal Property verification (FPV), Introduction to Model Checking | Class Notes, PDG: Ch 1 |
| 17. | 5th September 2023 | FPV: Consistency and Completeness of Properties | Class Notes, PDG: Ch 1 |
| 18. | 11th September 2023 | LTL | Class Notes, PDG: Ch 2, Huth: Ch 3 |
| 19. | 12th September 2023 | LTL, CTL | Class Notes, PFG: Ch 2, Huth: Ch 3 |
| 20. | 13th September 2023 | CTL, LTL vs CTL | Class Notes, PDG: Ch 2, Huth: Ch 3 |
| 21. | 25th September 2023 | CTL Model Checking Algorithm | Class Notes, Huth: Ch 3 |
| 22. | 26th September 2023 | CTL Model Checking Algorithm | Class Notes, Huth: Ch 3 |
| 23. | 27th September 2023 | Guest Lecture on by Dr. Disha Puri, Intel | Tacking design complexity through Formal Verification on Industrial Strength Designs |
| 24. | 3rd October 2023 | Correctness of CTL model Checking Algorithms | Class Notes, Huth: Ch 3 |
| 25. | 4th October 2023 | LTL Model Checking, Buchi Automata, NBA, GNBA | Class Notes, Huth: Ch 3, PDG: Ch 3 |
| 26. | 6th October 2023 | LTL to GNBA Construction | Class Notes, Huth: Ch 3, PDG: Ch 3 |
| 27. | 9th October 2023 | Verification Assertion generation with LLM - Demonstration | |
| 28. | 10th October 2023 | LTL Model Checking Algorithm | Class Notes, Huth: Ch 3, PDG: Ch 3 |
| 29. | 11th October 2023 | Complexity Reduction of Model Checking | Class Notes, Huth: Ch 3, PDG: Ch 3 |
| 30. | 16th October 2023 | Symbolic Model Checking | Class Notes, Huth: Ch 3, PDG: Ch 3 |
| 31. | 17th October 2023 | BDD based Symbolic Model Checking | Class Notes, PDG: Ch 3 |
| 32. | 18th October 2023 | BDD based Symbolic Model Checking | Class Notes, PDG: Ch 3 |
| 33. | 19th October 2023 | Project Evaluation Phase 1 | |
| 34. | 30th October 2023 | Quiz 2 | |
| 35. | 31st October 2023 | SAT based Symbolic Model Checking | Class Notes, PDG: Ch 3 |
| 36. | 1st November 2023 | SAT based Symbolic Model Checking | Class Notes, PDG: Ch 3 |
| 37. | 6th November 2023 | Project Evaluation Phase 2 (Groups 22, 6, 11, 20, 17, 7, 14, 35, 28) | |
| 38. | 6th November 2023 | Project Evaluation Phase 2 (Groups 25, 1, 24, 15, 16, 18, 27, 19, 33) | |
| 39. | 7th November 2023 | Project Evaluation Phase 2 (Groups 30, 12, 21, 2, 26, 10, 31, 9, 3) | |
| 40. | 7th November 2023 | Project Evaluation Phase 2 (Groups 4, 5, 8, 23, 34, 29, 32) | |
| 41. | 16th November 2023 | Project Evaluation Phase 3 (Groups 22, 6, 11, 20, 17, 7, 14, 35, 28) | |
| 42. | 16th November 2023 | Project Evaluation Phase 3 (Groups 25, 1, 24, 15, 16, 18, 27, 19, 33) | |
| 43. | 17th November 2023 | Project Evaluation Phase 3 (Groups 30, 12, 21, 2, 26, 10, 31, 9, 3) | |
| 44. | 17th November 2023 | Project Evaluation Phase 3 ((Groups 4, 5, 8, 23, 34, 29, 32) | |