CP7015 MODEL CHECKING AND PROGRAM VERIFICATION

 CP7015      MODEL CHECKING AND PROGRAM VERIFICATION

UNIT I            AUTOMATA AND TEMPORAL LOGICS

Automata on finite words – model checking regular properties – automata on infinite words – Buchi automata – Linear Temporal Logic (LTL) – automata based LTL model checking – Computational Tree Logic (CTL) – CTL model checking – CTL* model checking  

UNIT II        TIMED AND PROBABILISTIC TREE LOGICS

Timed automata – timed computational tree logic (TCTL) – TCTL model checking – probabilistic systems – probabilistic computational tree logic (PCTL) – PCTL model checking – PCTL* - Markov decision processes  

UNIT III        VERIFYING DETERMINISTIC AND RECURSIVE PROGRAMS

Introduction to program verification – verification of “while” programs – partial and total correctness – verification of recursive programs – case study: binary search – verifying recursive programs with parameters  

UNIT IV       VERIFYING OBJECT-ORIENTED AND PARALLEL PROGRAMS

Partial and total correctness of object-oriented programs – case study: Insertion in linked lists – verification of disjoint parallel programs – verifying programs with shared variables – case study: parallel zero search – verification of synchronization – case study: the mutual exclusion problem 

UNIT V       VERIFYING NON-DETERMINISTIC AND DISTRIBUTED PROGRAMS

Introduction to non-deterministic programs – partial and total correctness of non-deterministic programs – case study: The Welfare Crook Problem – syntax and semantics of distributed programs – verification of distributed programs – case study: A Transmission Problem – introduction to fairness

REFERENCES: 

1. C. Baier, J.-P. Katoen, and K. G. Larsen, “Principles of Model Checking”, MIT Press, 2008. 

2. E. M. Clarke, O. Grumberg, and D. A. Peled, “Model Checking”, MIT Press, 1999. 

3. M. Ben-Ari, “Principles of the SPIN Model Checker”, Springer, 2008. 

4. K. R. Apt, F. S. de Boer, E.-R. Olderog, and A. Pnueli, “Verification of Sequential and Concurrent Programs”, Third Edition, Springer, 2010. 

5. M. Huth and M. Ryan, “Logic in Computer Science --- Modeling and Reasoning about Systems”, Second Edition, Cambridge University Press, 2004. 

6. B. Berard et al., “Systems and Software Verification: Model-checking techniques and tools”, Springer, 2010. 

7. J. B. Almeida, M. J. Frade, J. S. Pinto, and S. M. de Sousa, “Rigorous Software Development: An Introduction to Program Verification”, Springer, 2011.