Tools

Verification

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.

RVHyper is a runtime verification tool for temporal hyperproperties.
RTLola 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.