CP7015 MODEL CHECKING AND PROGRAM VERIFICATION Syllabus - ME CSE Regulation 2013 2nd Semester Syllabus - www.annauniv.edu
OBJECTIVES:
To understand automata for model checking
To understand LTL, CTL, and CTL*
To understand timed automata, TCTL, and PCTL
To understand verification of deterministic and recursive programs
To understand verification of object-oriented programs
To understand verification of parallel, distributed, and non-deterministic programs
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 nondeterministic 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
OUTCOMES:
Upon Completion of the course,the students will be able to
Perform model checking using LTL
Perform model checking using CTL
Perform model checking using CTL*
Perform model checking using TCTL and PCTL
Verify deterministic and recursive programs
Verify object-oriented programs
Verify parallel, distributed, and non-deterministic programs
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.
ADS HERE !!!