
veriT

VeriT is an open, trustable and efficient SMT (Satisfiability Modulo Theories) solver. It comprises a SAT (propositional satisfiability) solver, an efficient decision procedure for uninterpreted symbols based on congruence closure, a simplexbased decision procedure for linear arithmetic, and instantiationbased quantifier reasoning.


Pascal Fontaine (Pascal.Fontaine@inria.fr)

Pascal Fontaine (Pascal.Fontaine@loria.fr), HansJörg Schurr (hansjorg.schurr@inria.fr), Sophie Tourret (sophie.tourret@loria.fr)

MODEL, VERIDIS

http://www.veriTsolver.org


SPASS

The classic SPASS is an automated theorem prover based on superposition that handles firstorder 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 bottomup 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.SPASS 3.9 has been used as the basis for SPASSAR, a new approximation refinement theorem proving approach.


Christoph Weidenbach (weidenbach@mpiinf.mpg.de)


VERIDIS

http://www.spassprover.org/


SPASSSATT

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 stateofthe art solvers. Furthermore, we have developed a new calculus and first prototypical implementation of a SAT solver with mixed OR/XOR clauses and are currently adapting our algorithms to support SUPERLOG reasoning.


Martin Bromberger (mbromber@mpiinf.mpg.de)

Martin Bromberger (mbromber@mpiinf.mpg.de), Mathias Fleury (mathias.fleury@mpiinf.mpg.de), Christoph Weidenbach (weidenbach@mpiinf.mpg.de)

VERIDIS

https://www.mpiinf.mpg.de/departments/automationoflogic/software/spassworkbench/spasssatt/


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 firstorder formulas.Redlog generally works with interpreted firstorder logic in contrast to free firstorder logic. Each firstorder formula in Redlog must exclusively contain atoms from one particular Redlogsupported theory, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlogsupported theories include Nonlinear Real Arithmetic (Real Closed Fields), Presburger Arithmetic, Parametric QSAT (quantified satisfiability solving), and many more.


Thomas Sturm (sturm@redlog.eu)

Thomas Sturm (sturm@redlog.eu)

VERIDIS

https://www.redlog.eu/


SPIKE

SPIKE, an automatic inductionbased 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 nontrivial applications and prototyped different proof experiments and extensions. The recent paper 'SPIKE, an automatic theorem prover – revisited' (HAL id hal02965319) gives an overview and may also serve as a user manual.


Sorin Stratulat (sorin.stratulat@loria.fr)

Sorin Stratulat (sorin.stratulat@loria.fr)

VERIDIS

https://github.com/sorinica/spikeprover/wiki


Nunchaku

Nunchaku is a model finder (counterexample generator) for higherorder logic.

Nunchaku is a model finder for higherorder 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 stateoftheart model finders and other solvers as backends.

Jasmin Blanchette (jasminchristian.blanchette@inria.fr)

Jasmin Blanchette (jasminchristian.blanchette@inria.fr), Simon Cruanes (simon.cruanes@inria.fr)

VERIDIS

https://github.com/nunchakuinria


TLAPS

TLAPS is a platform for developing and mechanically verifying proofs about
specifications written in the TLA+ language. 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 tableaubased prover Zenon
for firstorder 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 SMTlib 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), Ioannis Filippidis (ioannis.filippidis@inria.fr)

VERIDIS, CAMBIUM

https://tla.msrinria.inria.fr/tlaps/content/Home.html


Apalache

Version 0.5.0 implements a symbolic bounded model checker for \tlaplus{} that runs under the same assumptions as the explicitstate 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.

Apalache is a symbolic model checker that works under the following assumptions:(1) As in TLC, all specification parameters are fixed and finite, e.g., the system is initialized integers, finite sets, and functions of finite domains and codomains.
(2) As in TLC, all data structures evaluated during an execution are finite, e.g., a system specification cannot operate on the set of all integers.
(3) Only finite executions up to a given bound are analysed.In 2019, we have simplified the set of rewriting rules, which are used in the translation from TLA+ to SMT. We have shown that the rules are sound, that is, that the translator produces a set of SMT constraints that are equisatisfiable to the given TLA+ formula. We have conducted the experiments on 10 TLA+ specifications of distributed algorithms. When running bounded model checking, Apalache outperforms TLC in some cases. When checking inductive invariants, Apalache runs significantly faster than TLC. These results were reported at ACM OOPSLA 2019.
Apalache translates bounded executions of a TLA+ specifications into a set of quantifierfree SMT constraints. By querying the SMT solver, the model checker either finds a counterexample to an invariant, or proves that there is no counterexample up to given computation length.

Igor Konnov (igor.konnov@inria.fr)


VERIDIS

https://github.com/informalsystems/apalache


ByMC

ByMC implements several techniques for the parameterized verification of thresholdguarded distributed algorithms such as reliable broadcast, onestep Byzantine consensus, nonblocking atomic commit, conditionbased 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 thresholdguarded 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$.ByMC supports a parallel mode, which allows one to run verification experiments in an MPI cluster such as Grid5000 and Vienna Scientific Cluster.

Igor Konnov (igor.konnov@inria.fr)


VERIDIS

https://forsyte.at/software/bymc/


IMITATOR

IMITATOR is a software tool for parametric verification and robustness analysis of realtime systems with parameters. It relies on the formalism of networks of parametric timed automata, augmented with integer variables and stopwatches.


Etienne Andre (etienne.andre@loria.fr)

Etienne Andre (etienne.andre@loria.fr), Jaime Eduardo Arias Almeida (jaimeeduardo.ariasalmeida@inria.fr)

VERIDIS

https://www.imitator.fr/
