CP7015 MODEL CHECKING AND PROGRAM VERIFICATION SYLLABUS FOR M.E COMPUTER SCIENCE AND ENGINEERING REG 2013 SEMESTER 2 - Anna University Internal marks 2018

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.

No comments:

Post a Comment