Automata Tutor

Automata Tutor is a tool that helps teachers and students in large courses on automata and formal languages. Automata Tutor supports automated grading and personal feedback generation for many exercise types about NFAs, DFAs, regular expressions, context-free grammars, pushdown automata and Turing machines.

Owl

A Java tool collection and library for Omega-words, ω-automata and Linear Temporal Logic (LTL).

Peregrine

Population protocols are a model of computation intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to achieve a common task. Peregrine allows users to design protocols, to simulate them both manually and automatically, to gather statistics of properties such as convergence speed, and to verify correctness automatically.

Rabinizer

Rabinizer 4 is a tool set for generating small deterministic ω-automata from LTL (linear temporal logic) formulas.

SeQuaiA

A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks (CRNs)

Strix

Strix is a tool for reactive LTL synthesis.