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

 GPU-based Mean-Payoff Game Solver

 GPU-based Parity Game Solver
 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

 A Tool for Modal Transition Systems

 An Advanced Solver for Presburger Arithmetic

 Moped

 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. 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.