Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
 Chair for Foundations of Software Reliability and Theoretical Computer Science
 Tools

 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.

 Rabinizer
 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
 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: a majority protocol extends the minimal example with more options. By default, the simulator is loaded with this file. 0modulo3.txt atleast5.txt 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.