# Software

• veriT

• VeriT is an open, trustable and efficient SMT (Satisfiability Modulo Theories) solver, featuring efficient decision procedure for uninterpreted symbols and linear arithmetic, and quantifier reasoning.

• veriT comprises a SAT solver, a decision procedure for uninterpreted symbols based on congruence closure, a simplex-based decision procedure for linear arithmetic, and instantiation-based quantifier handling.

• Pascal Fontaine (Pascal.Fontaine@inria.fr)

• Haniel Barbosa (haniel.barbosa@inria.fr), Daniel El Ouraoui (daniel.el-ouraoui@inria.fr), Pascal Fontaine (Pascal.Fontaine@loria.fr), Hans-Jörg Schurr (hans-jorg.schurr@inria.fr)

• MODEL, VERIDIS
• SPASS

• SPASS is an automated theorem prover based on superposition that handles first-order logic with equality and several extensions for particular classes of theories.

• The classic SPASS is an automated theorem prover based on superposition that
handles first-order logic with equality and several extensions for particular
classes of theories. With version SPASS 3.9 we have stopped the development of the classic prover and have started the bottom-up development of SPASS 4.0 that will actually be a workbench of automated reasoning tools. Furthermore, we use SPASS 3.9 as a test bed for the development of new calculi.

Meanwhile we have released the second version of SPASS-IQ, our solver for
linear integer arithmetic that we are currently extending to real and mixed real-integer arithmetic.

SPASS 3.9 has been used as the basis for SPASS-AR, a new approximation refinement theorem proving approach.

• Christoph Weidenbach (weidenbach@mpi-inf.mpg.de)

• VERIDIS
• SPASS-SATT

• SPASS-SATT is an SMT solver for linear integer arithmetic, mixed linear arithmatic and rationall linear arithmetic.

• SPASS -SATT is an SMT solver for the theories of linear integer arithmetic, linear rational
arithmetic and mixed linear arithmetic. It features new tests for the satisfiability of unbounded
systems, as well as new algorithms for the detection of integer solutions.

We further investigated the use of redundancy elimination in SAT solving and underlying implementation techniques. Our aim is a new approach to SAT solving that needs fewer conflicts (on average) \emph{and} is faster than the current state-of-the art solvers. Furthermore, we have developed a new calculus and first prototypical implementation of a SAT solver with mixed OR/XOR clauses.

• Martin Bromberger (martin.bromberger@loria.fr)

• Martin Bromberger (martin.bromberger@loria.fr), Mathias Fleury (mathias.fleury@loria.fr), Christoph Weidenbach (christoph.weidenbach@loria.fr)

• VERIDIS
• Redlog

• Redlog is an integral part of the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation by supplying more than 100 functions on first-order formulas.

Redlog generally works with interpreted first-order logic in contrast to free first-order logic. Each first-order formula in Redlog must exclusively contain atoms from one particular Redlog-supported theory, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlog-supported theories include Nonlinear Real Arithmetic (Real Closed Fields), Presburger Arithmetic, Parametric QSAT, and many more.

• Redlog is an integral part of the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation by supplying more than 100 functions on first-order formulas.

Redlog generally works with interpreted first-order logic in contrast to free first-order logic. Each first-order formula in Redlog must exclusively contain atoms from one particular Redlog-supported theory, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlog-supported theories include Nonlinear Real Arithmetic (Real Closed Fields), Presburger Arithmetic, Parametric QSAT, and many more.

• Thomas Sturm (sturm@redlog.eu)

• Thomas Sturm (sturm@redlog.eu)

• VERIDIS
• SPIKE

• Automated induction-based theorem prover

• SPIKE, an automatic induction-based theorem prover built to reason on conditional theories with equality, is one of the few formal tools able to perform automatically mutual and lazy induction. Designed in the 1990s, it has been successfully used in many non-trivial applications and served as a prototype for different proof experiments and extensions.

• Sorin Stratulat (sorin.stratulat@loria.fr)

• Sorin Stratulat (sorin.stratulat@loria.fr)

• VERIDIS

• Nunchaku

• Nunchaku is a model finder (counterexample generator) for higher-order logic.

• Nunchaku is a model finder for higher-order logic, with dedicated support for various definitional principles. It is designed to work as a backend for various proof assistants (notably Isabelle/HOL and Coq) and to use state-of-the-art model finders and other solvers as backends.

• Jasmin Christian Blanchette (jasmin-christian.blanchette@inria.fr)

• Jasmin Christian Blanchette (jasmin-christian.blanchette@inria.fr), Simon Cruanes (simon.cruanes@inria.fr)

• VERIDIS
• TLAPS

• TLAPS is a platform for developing and mechanically verifying proofs about TLA+
specifications. The TLA+ proof language is hierarchical and explicit, allowing a
user to decompose the overall proof into proof steps that can be checked
independently. TLAPS consists of a proof manager that interprets the proof
language and generates a collection of proof obligations that are sent to
backend verifiers. The current backends include the tableau-based prover Zenon
for first-order logic, Isabelle/TLA+, an encoding of TLA+ set theory as an
object logic in the logical framework Isabelle, an SMT backend designed for use
with any SMT-lib compatible solver, and an interface to a decision procedure for
propositional temporal logic.

• Stephan Merz (Stephan.Merz@loria.fr)

• Damien Doligez (damien.doligez@inria.fr), Stephan Merz (stephan.merz@loria.fr)

• GALLIUM, VERIDIS
• Apalache

• The first version implements a symbolic bounded model checker for \tlaplus{} that runs under the same assumptions as the explicit-state model checker TLC. It checks whether a \tlaplus{} specification satisfies an invariant candidate by checking satisfiability of an SMT formula that encodes: (1) an execution of bounded length, and (2) preservation of the invariant candidate in every state of the execution. Our tool is still in the experimental phase, due to a number of challenges posed by the semantics of \tlaplus{} to SMT solvers.

• Igor Konnov (igor.konnov@inria.fr)

• VERIDIS
• ByMC

• ByMC implements several techniques for the parameterized verification of threshold-guarded distributed algorithms such as reliable broadcast, one-step Byzantine consensus, non-blocking atomic commit, condition-based consensus, and randomized consensus. The tool accepts two kinds of inputs: (i) threshold automata (the framework of our verification techniques) and (ii) Parametric Promela (which is similar to the way in which the distributed algorithms are presented in the distributed computing literature). Internally, the tool analyzes representative executions by querying an SMT solver. Apart from verification, ByMC also implements a technique for the automatic synthesis of threshold guards.

The tool can run on a single computer as well as in an MPI cluster, e.g., Grid5000 or Vienna Scientific Cluster.

• In recent work, we have introduced a series of techniques for automatic verification of threshold-guarded distributed algorithms that have the following features: (1) up to $t$ of $n$ processes may exhibit crash or Byzantine failures, (2) the correct processes count messages and progress when they receive sufficiently many messages, e.g., at least $t + 1$, (3) the number $n$ of processes in the system is a parameter, as well as $t$, (4) and the parameters are restricted by a resilience condition, e.g., $n > 3t$.

• Igor Konnov (igor.konnov@inria.fr)

• VERIDIS