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 2017

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

The following tools are used in the lectures and in the exercises.

  • Spin
     
  • NuSMV
     
  • DDcal can be downloaded from the web page of Fabio Somenzi.

    Follow the instructions in INSTALL to build the package.

    If you have a problem when installing the default version of perl/Tk from CPAN, download the lastest version Tk-804.033 and install it manually.

  • Moped

    To quickly get started using Moped, you might want to use Docker with this pre-compiled image.

Here you can find specification patterns in LTL and other formalisms.