Wiki Agenda Contact Version française

Automated Reasoning

Overview

CiME/Coccinelle chain Historically, automated reasoning is divided into two main streams, the first one is based on resolution, rewriting and unification techniques, and the second one on the combination of decision procedures. 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. More recently, we have been interested in the second approach, and we started the development of the SMT prover Alt-Ergo. One of our current goals is to integrate rewriting techniques at the very heart of Alt-Ergo, in order to increase both its efficiency and expressivity.


Alt-Ergo tools

Thematics

Rewriting

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. For instance, the following system models the non-abelian groups using the usual mathematical definition:
(x . y) . z=x . (y . z)                     (A)
x . e=x(N)
x . i(x)=e(I)
Whith these equalities, it is possible to prove that i(e) = e by the following steps:
i(e)=Ni(e) . e 
 =Ii(e) . (i(e) . i(i(e))) 
 =Ni(e) . (i(e) . i(i(e).e)) 
 =Ii(e) . (i(e) . i(i(e).(e.i(e)))) 
 =Ai(e) . (i(e) . i((i(e).e).i(e))) 
 =Ni(e). (i(e) . i( i(e).i(e) )) 
 =A(i(e). i(e)) . i( i(e).i(e) )) 
 =Ie
Restricting the above set of equalities to the rewriting system displayed below raises several issues.
(x . y) . z→x . (y . z)                     (A)
x . e→x(N)
x . i(x)→e(I)
First, it is no longer possible to prove that i(e) = e, since none of the two terms can be reduced. The second problem is how to garantee that reducing as far as possible a term will eventually yield a result in a finite time. The corresponding properties are kown as confluence and termination. Completion is a way of recovering confluence, but the process may not terminate, and yields only a semi-decision procedure. Since the last decade, termination is a very active area in automated deduction: numerous criteria have been proposed, and implemented in several tools. Since 2003, there is a termination competition which reveals that every participant tool has at least once used a non valid argument in its proofs.
We work on how to certify some of the algorithms used in rewriting tools, and also some properties of rewriting systems, such as equality modulo and termination. For that purpose, we developp Coccinelle, the Coq companion library of our rewriting tool box CiME. Coccinelle features the Coq modelling of : Hence Coccinelle can be used to check that a termination certificate is valid, that is when a theorem is applied, all its premises are fullfilled.

Combination of Decision Procedures

Alt-Ergo is an SMT (Satisfiability Modulo Theory) solver dedicated to program verification. The input syntax of Alt-Ergo is a first order logic extended with predefined theories and polymorphic types. The built-in theories of Alt-Ergo are the following:

People

François Bobot, Sylvain Conchon, Évelyne Contejean, Claire Dross, Mohamed Iguernelala, Alain Mebsout, Andrei Paskevich, Xavier Urbain

Tools

Grants

Main publications

[1]
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Saarbrücken, Germany, April 2011. Springer. [ bib ]
[2]
Stéphane Lescuyer and Sylvain Conchon. Improving Coq propositional reasoning using a lazy CNF conversion scheme. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of Combining Systems, 7th International Symposium, Proceedings, volume 5749 of Lecture Notes in Computer Science, pages 287-303, Trento, Italy, September 2009. Springer. [ bib | DOI ]
[3]
François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 1-5, 2008. [ bib | PDF | .pdf ]
[4]
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. CC(X): Semantical combination of congruence closure with solvable theories. In Proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), volume 198-2 of Electronic Notes in Computer Science, pages 51-69. Elsevier Science Publishers, 2008. [ bib ]
[5]
Stéphane Lescuyer and Sylvain Conchon. A reflexive formalization of a SAT solver in Coq. In Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, 2008. [ bib ]