Automated Reasoning


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.


Former contributor: Alain Mebsout, David Declerck, Xavier Urbain.

Research axes

Rewriting and termination

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.

Satisfiability Modulo Theories

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.

Model Checking Modulo Theories

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.

Link with interactive theorem proving

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.


  • ANR Pardi: The objective of PARDI is the formal, machine-supported verification of parameterized distributed systems.
  • FUI LCHIP: The main objective of the LCHIP project (Low Cost High Integrity Platform) is to ease development of safety critical systems and software up to SIL4, the highest Safety Integrated Level.
  • ANR Soprano: This project aims at preparing the next generation of verification-oriented solvers by gathering experts from academia and industry.
Former grants:
  • ANR Cafein
  • ANR Bware
  • ANR Decert
  • FUI Hi-Lite

Software and proofs

  • CiME: a rewriting tool box
  • Coccinelle: the CiME Coq library companion
  • Gappa: a tool for automatically verifying properties on numerical programs dealing with floating-point or fixed-point arithmetic
  • Alt-Ergo: an open-source SMT solver
  • Cubicle: an open source SMT-based model checker
  • SMTCoq : a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers.