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!

Please follow this link

Please follow this link

Please follow this link

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

Please follow this link

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

Please follow this link

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

Please follow this link

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.