Advanced Techniques in Verification (Techniques de Vérification Avancées)
Master 2 Recherche Informatique

Homework

• Homework due 21/112016

Content and links to lecture notes

• Part I: Computation Tree Logic for formal verification , CTL with fairness constraints , ROBDD (Mondays, Sophie Pinchinat),
• Part II: Timed and Probabilistic extensions of Computation Tree Logic (Wednesdays, Blaise Genest)

Bibliography

• Automata, logics, and infinite games: A guide to current research.
  Eds : Grädel E., Thomas W., Wilke T., outcome of a Dagstuhl seminar, February 2001, Springer, ISBN 3-540-00388-6, 2002.
• Principles of Model-checking. C. Baier and J.-P. Katoen. MIT Press, 2009.
• The Complexity of Temporal Logic Model Checking. Philippe Schnoebelen. Advances in Modal Logic 2002: 393-436.
• Vérification de logiciels: Techniques et outils du model-checking. Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie and A. Petit. Vuibert, 1999.
• Temporal verification of Reactive Systems: Safety. Z. Manna and A. Pnueli. Springer Verlag, 1995.
• Model-checking. E.M. Clarke, O. Grunberg and D. Peled. MIT Press, 2000.

Assessment

• homework 50%
• examination 50%

Additional material

• notes on Tarski-Knaster Theorem

Schedule

See your ENT .