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
Model-Checking SS 2020

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


Exercise Sheets

  • 1. Introduction
    Exercise sheet: [PDF] | [Solutions]
    Some useful links: Spin README Spin references Modex
  • 2. Propositional Logic and Kripke Structures
    Exercise sheet: [PDF] | [Solutions]
  • 3. Linear temporal logic (LTL)
    Exercise sheet: [PDF] | [Solutions]
  • 4. More LTL, Spot and Büchi Automata
    Exercise sheet: [PDF] | [Solutions]
    Spot is available at spot.lrde.epita.fr/app
  • 5. LTL and Büchi
    Exercise sheet: [PDF] | [Solutions]
  • 6. Partial Order Reduction
    Exercise sheet: [PDF] | [Solutions]
  • 7. Computation tree logic (CTL)
    Exercise sheet: [PDF] | [Solutions]
  • 8. CTL and NuSMV
    Exercise sheet: [PDF] | [ 8.1 SMV code, 8.2 SMV code, 8.3 SMV code]
  • 9. Binary Decision Diagrams
    Exercise sheet: [PDF] | [Solutions]
  • 10. Simulation and bisimulation
    Exercise sheet: [PDF] | [Solutions]
  • 11. Abstraction-Refinement
    Exercise sheet: [PDF] | [Solutions]
  • 12. Pushdown systems
    Exercise sheet: [PDF] | [Solutions]