| CS60030 Formal Systems | SPRING 2021, L-T-P: 3-1-0 |
Schedule
Instructor Prof. Pallab Dasgupta
Timing MON (12:00–12:55), TUE (10:00–11:55), THURS (8:00–8:55) Venue Microsoft Teams : Class Link Teaching Assistants Briti Gangopadhyay (briti_gangopadhyay@iitkgp.ac.in),
Sayandeep Sanyal (sayandeep.sanyal@gmail.com),
Sudipa Mandal (contacttosudipamandal@gmail.com),
Announcements
- First Class Test - 25th January | Syllaybus - Upto Symbolic Reachability
- Third Class Test - 30th March 6PM - 7PM | Syllaybus - Program Verification and CEGAR
- Fourth Class Test - 13th April 5PM - 7PM | Syllaybus - Timed and Hybrid Automata
Syllabus
- Introduction
- Succinct Representations
- Symbolic Reachability
- Specification Formalisms
- Omega Regular Languages and Buchi Automata
- Model Checking
- Scalability in Model Checking
- Program Verification
- Timed Automata
- Hybrid Automata
Books and References
[1] Pallab Dasgupta A Roadmap for Formal Property Verification, Springer, 2006 [2] Christel Baier and Joost-Pieter Katoen Principles of Model Checking, MIT Press, 2008. [3] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem Handbook of Model Checking, Springer, 2019 [4] Rajeev Alur Principles of Cyber-Physical Systems, MIT Press, 2015 Online Material
Week Topic Chapter Tutorial Week 1 Introduction Introduction Introduction Succinct Representations Succinct Representations Succinct Representations Tutorial 1 Tutorial on SAT and BDD Tutorial on SAT and BDD Week 2 Tutorial 2 Hands on CUDD Hands on CUDD Week 3 Symbolic Reachability Symbolic Reachability Symbolic Reachability Tutorial 3 Tutorial on CF and Symbolic Reachability Tutorial on CF and Symbolic Reachability Week 4 Specification Formalisms Specification Formalisms Specification Formalisms Week 5 Omega Regular Languages and Buchi Automata Omega Regular Languages and Buchi Automata Omega Regular Languages and Buchi Automata Tutorial 4 Tutorial on LTL and CTL Tutorial on LTL and CTL Week 6 Tutorial 5 Tutorial 05 Omega-Regular Languages & Buchi automata Omega-Regular Languages & Buchi automata Week 7 Model Checking Model Checking Model Checking Week 8 Scalability in Model Checking Scalability in Model Checking Scalability in Model Checking Week 9 Program Verification Program Verification Program Verification Week 10 Tutorial 6 Tutorial on Program Verification Tutorial 06 Program Verification Week 11 Timed Automata Timed Automata Timed Automata Week 12 Hybrid Automata Hybrid Automata Hybrid Automata Week 12-13 Tutorial 7 Tutorial on Timed and Hybrid Atomata Tutorial 07 Timed and Hybrid Atomata Previous course pages: 2020 | 2019
| CS60030 Formal Systems | Spring 2021, L-T-P: 3-1-0 |