Guillaume Bury - R&D Engineer

mSAT is a modular SAT Solver written in OCaml. It is based on alt-ergo-zero, a standalone version of the SAT solver used at one point in the automated theorem prover alt-ergo. mSAT provides an ocaml functor to create an SMT Solver with user-defined types for terms and formulas, and solving functions. Instantiating the functor with an empty solving function results in a pure SAT solver. mSAT also implements the McSat calculus.

Dolmen is an OCaml library that provides parsers for some languages used in automated deduction, such as TPTP and SMTLib. Besides providing already written up-to-date parsers, another benefit of Dolmen is to document the various term structure needed for each language, and to provide an adequate implementation that meets these requirements.

Zenon Arith is an extension of the tableaux-based automated theorem prover Zenon. This extension uses the simplex algorithm as a decision procedure to solve problems over rationals, and a branch-and-bound approach to solve problems over integers. This extension is also able to handle real linear arithmetic, which actually coincides with the rational fragment of linear arithmetic due to the syntactical restrictions of the TPTP input format for reals. This extension is able to output proof scripts for the Coq proof assistant for automated verification.

Ocaml-simplex is an ocaml implementation of the simplex algorithm. It currently only check for satisfiability of linear systems, but can outptu proof certificates for unsatisfiable results. It is the decision procedure used in the Zenon-Arith theorem prover.

Frog-utils provides tools and libraries (in OCaml) for scheduling and running jobs on a shared computer, and then analyse their output. It also includes a tool that aims to ease the process of benchmarking automated theorem provers and storing their result in an easy to read and use json file.