{{{credits}}}
| L | T | P | C |
| 3 | 0 | 0 | 3 |
- To understand the need of logics for specification and verification of computer systems
- To learn program correctness using Hoare Logic
- To learn the skill of writing formal specifications in LTL and CTL
- To learn model checking algorithms for LTL and CTL
- To learn model checking for Timed Systems.
{{{unit}}}
| UNIT I | FOUNDATIONS | 9 |
Propositional Logic: Syntax – Semantics – Natural deduction; Predicate Logic: Syntax – Semantics – Natural deduction; Linear-time Temporal Logic: Syntax – Semantics – Specifications in LTL; Branching-time Logic: Syntax – Semantics – Specifications in CTL; CTL* and the expressive powers of LTL and CTL.
{{{unit}}}
| UNIT II | HOARE LOGIC AND PROGRAM CORRECTNESS | 9 |
A Framework for Program Correctness: A core programming language – Hoare triples – Partial and total correctness – Program variables and logical variables; Proof Calculus for Partial Correctness: Proof rules – Proof tableaux; Proof Calculus for Total Correctness.
{{{unit}}}
| UNIT III | MODEL CHECKING | 9 |
Model-checking Algorithms: The CTL model-checking algorithm – CTL model checking with fairness – The LTL model-checking algorithm; CTL* Model-checking Algorithm; Model Checking using Automata; Checking Emptiness; Translating LTL into Automata; On-the-fly Model checking.
{{{unit}}}
| UNIT IV | SYMBOLIC MODEL CHECKING | 9 |
Binary Decision Diagrams: Representing Boolean formulas – Representing Kripke structures; Fixpoint Representations; Symbolic Model Checking for CTL; Fairness in Symbolic Model Checking; Counterexamples and Witnesses; Relational Product Computations; Symbolic Model Checking for LTL; NuSMV.
{{{unit}}}
| UNIT V | MODEL CHECKING TIMED SYSTEMS | 9 |
Timed Automata: Semantics – Time divergence – Timelock – Zenoness; Timed Computation Tree Logic; TCTL Model Checking: Eliminating timing parameters – Region transition systems – The TCTL model-checking algorithm; Model checkers for Timed Automata: UPPAAL – KRONOS.
\hfill Total Periods: 45
After the completion of this course, students will be able to:
- Explain, analyse and compare various model checking algorithms (K3)
- Prove partial correctness of simple programs using Hoare logic (K3)
- Write formal properties and specifications in CTL and LTL (K3)
- Specify and verify simple systems using NuSMV (K3)
- Specify and verify simple systems using UPPAAL (K3).
- M Huth, M Ryan, “Logic in Computer Science – Modeling and Reasoning About Systems”, 2nd Edition, Cambridge University Press, 2004. (Units I, II and III)
- Edmund Clarke, Orna Grumberg, Doron Peled, “Model Checking”, The MIT Press, 1999. (Units III and IV)
- C Baier, J Katoen, “Principles of Model Checking”, The MIT Press, 2008. (Unit V)
- Michael Clarke, Thomas Henzinger, Helmut Veith, Roderick Bloem, “Handbook of Model Checking”, Springer 2018
- Orna Grumberg, Helmut Veith, “25 Years of Model Checking: History, Achievements, Perspectives” Springer-Verlag, 2008
- Zohar Manna, Amir Pnueli, “Temporal Verification of Reactive Systems: Safety”, Springer-Verlag, 2012
- Krzysztof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog, “Verification of Sequential and Concurrent Programs”, Springer, 3rd edition, 2009
| PO1 | PO2 | PO3 | PO4 | PO5 | PO6 | PO7 | PO8 | PO9 | PO10 | PO11 | PO12 | PSO1 | PSO2 | PSO3 | ||
| K3 | K6 | K6 | K6 | K6 | K6 | K5 | K6 | |||||||||
| CO1 | K3 | 3 | 2 | 3 | 2 | |||||||||||
| CO2 | K3 | 3 | 2 | 2 | ||||||||||||
| CO3 | K3 | 3 | 2 | 2 | ||||||||||||
| CO4 | K3 | 3 | 2 | 2 | ||||||||||||
| CO5 | K3 | 3 | 2 | 3 | 3 | 2 | ||||||||||
| Score | 15 | 10 | 3 | 3 | 3 | 10 | ||||||||||
| Course Mapping | 3 | 2 | 3 | 3 | 3 | 2 |