- MCHyper is a model checker for hyperproperties.
- Arctor is a termination prover for multi-threaded programs.
- RESY is a requirement synthesis tool for compositional model checking.
- dvt is a deductive verification tool for concurrent reactive systems. It supports verification of LTL properties, proving refinement relations, and translation validation.
- SLAB is a certifying model checker for infinite state concurrent systems.
- BoSy is a reactive synthesis tool based on contraint solving.
- SyFCo is a tool for reading, manipulating and transforming synthesis specifications in TLSF.
- SafetySynth is synthesis tool based on solving safety games.
- Synthia is a verification tool for checking safety requirements of open real-time systems modeled as networks of timed automata.
- Unbeast synthesizes finite-state systems from LTL specifications using a symbolic implementation of the bounded synthesis approach.
- Bassist synthesizes finite-state systems from ACTL ∩ LTL specifications.
Automata & Monitoring
- RVHyper is a runtime verification tool for temporal hyperproperties.
- StreamLAB stream-based runtime monitoring.
- MoCS synthesizes monitor circuits from linear time temporal logic formulas.
- CirView is a small tool for 3D visualization of LTL path checking via boolean circuits.
- DBA Minimizer is a tool calling an external SAT solver successively to minimize deterministic Büchi automata.
- NBW Minimizer is a modified SAT-solver that performs minimization of non-deterministic Büchi automata.
- EAHyper is a satisfiability solver for hyperproperties.
- CAQE is a solver for quantified Boolean formulas in conjunctive normal form.
- QuAbS is a solver for quantified Boolean formulas in negation normal form.
- bunsat is a DQBF solver based on the bounded unsatisfiability method.
- Caissa is a decision procedure for the quantifier-free theories of equality with uninterpreted symbols, integer linear arithmetic, fixed-size bit-vectors, arrays, sets, multisets, and lists with a length function.