Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Home
 Contact
 Teaching
lectures
exercises
seminars
proseminars
research seminars
practical courses
WS 2020/21
SS 2020
WS 2019/20
SS 2019
WS 2018/19
SS 2018
WS 2017/18
SS 2017
WS 2016/17
SS 2016
WS 2015/2016
SS 2015
WS 2014/2015
SS 2014
WS 2013/2014
SS 2013
WS 2012/2013
SS 2012
WS 2011/2012
SS 2011
WS 2010/2011
SS 2010
WS 2009/2010
SS 2009
WS 2008/2009
SS 2008
WS 2007/2008
SS 2007
WS 2006/2007
SS 2006
WS 2005/2006
SS 2005
WS 2004/2005
SS 2004
Before 2004
 People
Publications
 Student Projects
Research
Tools
Heroes of Computer Science
 Help

































Model-Checking SS 2019

  News | Basic information | Content | Exercises | Slides | Links | Exam

Bonus Exercise

We invite highly motivated students to take part in the new and experimental Implement a Model Checker voluntary exercise!

Exercise Sheets

  • 1. Introduction
    Exercise sheet: [PDF] | [Solutions]
    Some useful links: Spin README Spin references Modex
  • 2. Linear temporal logic (LTL)
    Exercise sheet: [PDF] | [Solutions]
  • 3. More LTL and Spot
    Exercise sheet: [PDF] | [Solutions]
    Spot is available at spot.lrde.epita.fr/app
  • 4. Büchi Automata
    Exercise sheet: [PDF] | [Solutions]
  • 5. LTL and Büchi
    Exercise sheet: [PDF] | [Solutions]
    As discussed in class, some of the exercises in this sheet were problematic. An updated version would be uploaded in the coming weeks.
  • 6. Partial Order Reduction
    Exercise sheet: [PDF] | [Solutions]
  • 7. Computation tree logic (CTL)
    Exercise sheet: [PDF] | [Solutions]
  • 8. CTL and NuSMV
    Exercise sheet: [PDF] | [Solutions, 8.2 SMV code, 8.3 SMV code]
  • 9. Binary Decision Diagrams
    Exercise sheet: [PDF] | [Solutions]
  • 10. Abstraction, Simulation and bisimulation
    Exercise sheet: [PDF] | [Solutions]
  • 11. Pushdown systems
    Exercise sheet: [PDF] | [Solutions]
    Python script to compute Pre*: pre_star.py