I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Model-Checking SS 2018

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

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.