CP7015 MODEL CHECKING AND PROGRAM VERIFICATION SYLLABUS FOR M.E COMPUTER SCIENCE AND ENGINEERING REG 2013 SEMESTER 2

CP7015 MODEL CHECKING AND PROGRAM VERIFICATION SYLLABUS

M.E. COMPUTER SCIENCE AND ENGINEERING

SEMESTER II

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 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

TOTAL : 45 PERIODS

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.