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.
- Thibaut Balabonski
- Sylvain Conchon
- Evelyne Contejean
- Mohamed Iguernelala
- Chantal Keller
- Guillaume Melquiond
- Andrei Paskevich
- Fatiha Zaidi
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
Link with interactive theorem proving
- 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.
- ANR Cafein
- ANR Bware
- ANR A3PAT
- 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.