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

A Tool to for Probability Calculus

With this tool you can check statements that are common in introductory courses on probability theory, e.g. that pairwise independence does not imply mutual independence.
It checks satisfiability of formulae involving statements over probabilities.
Click here to try the tool!

FPsolve -- a generic solver for polynomial fixpoint equations

Please follow this link

GPU-based Mean-Payoff Game Solver

Please follow this link

GPU-based Parity Game Solver

Please follow this link

Online BDD Simulation Tool (obst)

Binary Decision Diagrams (BDDs, see also Wikipedia) are a compact way of representing sets of numbers, so that certain set operations (e.g. union, intersection, complement) can still be executed efficiently. They are used extensively in logic synthesis as well as formal verification.

obst is an application that shows how the algorithms for constructing and operating on BDDs work on a step-by-step basis. You can try it out here. It is intended to be useful for both exploring the inner workings of BDDs interactively, as well as demonstrating the intermediate steps of a BDD computation in a classroom environment.

A precompiled Linux x64 binary is available here. For the source code and further instructions, please visit the tool's website on GitHub.


The Rabinizer tool generates small deterministic Rabin automata from LTL formulae.
Please follow this link

A Tool for Modal Transition Systems

Please follow this link

An Advanced Solver for Presburger Arithmetic

Please follow this link


Moped is a model checker for pushdown systems. See the official web page for more information.

To quickly get started using Moped, download Docker and follow this link to get the image.

jMoped 2.0

jMoped is a test environment for Java programs written as an Eclipse plug-in.

Given a Java method, jMoped can simulate the execution of the program for all possible arguments within a finite range and generate coverage information for these executions. Moreover, it checks for some common Java errors, i.e. assertion violations, null pointer exceptions, and array bound violations. When an error is found, jMoped finds out the arguments that lead to the error. A JUnit test case can also be automatically generated for further testing.

For more details, please follow this link

HSF(C): A Software Verifier based on Horn Clauses

Please follow this link

A Conversion Game Extension for JFLAP

A game, based on JFLAP, lets you play with conversions between various representations of regular and ω-regular languages.

For more details, please follow this link

Workflow Analyzer

Please follow this link

Simpol - A Simulator for Population Protocols

Please follow this link.

Population protocols are a model of distributed computation by a collection (or population) of anonymous agents. Agents interact with one another to carry out computations according to transition functions. For background information of the tool, see the paper by Aspnes and Ruppert.

The simulator requires a configuration file. The file, written in JavaScript and JSON, should at least define states and rules between pairs of states. Download a minimal example to see the syntax, or the following more flexible examples:

The simulator supports 3 modes. Depending on the mode, a step simulates one of the following actions:

  • Sequential: Randomly pick a pair of states with an applicable rule, and apply the rule.
  • Sequential Timed: Randomly pick a pair of states regardless of rules, and apply a rule is possible.
  • Parallel: Randomly pick all pairs of states, and apply rules to all applicable pairs.
Clicking run triggers a series of steps until no applicable pairs are available.