In the VALS team, we are interesting in several domains related to automated reasoning. In particular, we are working on rewriting and termination techniques, SMT (Satisfiability Modulo Theories) solvers, and model checking.

For twenty years, our team has been working on rewriting and has developed the rewriting tool box CiME, as well as its Coq certification library Coccinelle. Term rewriting is a way to tackle equality in the automated deduction field: whereas an equation can be used in either directions, a rewriting rule can be used only from left to right. Termination is key issue since it ensures that the computations eventually end with a result.

Verifying that a program meets formal specifications typically amounts to generating verification conditions e.g.~using a weakest precondition calculus. These verification conditions are purely logical formulas–typically in first-order logic and involving arithmetic in integers or real numbers–that should be checked to be true. This can be done using automatic provers, in particular, SMT solvers are generic provers well-suited for automatically discharging such verification conditions. In VALS, we are developping our own SMT solver, called Alt-Ergo.

In VALS, we are developping a new symbolic model checker, called Cubicle, for verifying safety properties of parameterized transition systems. The input language of Cubicle allows to describe a restricted class of parameterized systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. The theoretical framework behind Cubicle is Model Checking Modulo Theories (MCMT) designed by S. Ghilardi and S. Ranise.

To take advantages of both automated and interactive reasoning in a same system, we develop SMTCoq, a plugin for the Coq proof assistant to interact with external automatic provers based on satisfiability (SAT and SMT). The heart of SMTCoq is a generic proof checker for a modular certificate format, which can be applied at small cost to state-of-the-art proof-producing provers; currently supporter solvers are ZChaff, CVC4 and veriT. The objectives are (1) to efficiently and reliably check large combinatorial proofs that make use of satisfiability solvers and (2) to safely increase the automation of the Coq proof assistant.