Peregrine

A tool the design, parameterized verification and simulation of population protocols. Try the online demo!

Find out more!

Strix

A tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games. Try the online demo!

Find out more!

More

We are currently developing more tools for parametrized verification and synthesis …

Contribute!