Tools

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

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

• MoCS synthesizes monitor circuits from linear time temporal logic formulas.

• SLAB is a certifying model checker for infinite state concurrent systems.

• CirView is a small tool for 3D visualization of LTL path checking via boolean circuits.

• Unbeast synthesizes finite-state systems from LTL specifications using a symbolic implementation of the bounded synthesis approach.

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

• Synthia is a verification tool for checking safety requirements of open real-time systems modeled as networks of timed automata.