Contact English version

L'équipe ProVal s'est arrêtée à la fin août 2012, et renaît en une nouvelle équipe Toccata
Ces pages n'évoluent plus, suivez le lien ci-dessus pour les informations à jour sur notre équipe.

Démonstration automatique

Présentation

CiME/Coccinelle chain Historiquement, la démonstration automatique est divisée en deux courants principaux, celui qui est basé sur les techniques de résolution, de récriture et d'unification, et celui basé sur la combinaison de procédures de décision. Depuis une vingtaine d'années, notre équipe travaille sur la récriture et a développé la boîte à outils CiME, puis sa bibliothèque de certification en Coq Coccinelle. Plus récemment, nous nous sommes intéressés à la seconde approche, en développant le démonstrateur Alt-Ergo. Un de nos objectifs actuels est d'intégrer des techniques de récriture au coeur même d'Alt-Ergo, afin d'augmenter sa puissance et son expressivité.


Alt-Ergo tools

Thématiques

Récriture

La récriture de termes est une technique pour traiter l'égalité en démonstration automatique : alors qu'une équation peut être utilisée dans les deux sens, une règle de récriture ne peut s'appliquer que de gauche à droite. Par exemple, le système ci-dessous modélise les groupes non commutatifs suivant la définition mathématique usuelle :
(x . y) . z=x . (y . z)                     (A)
x . e=x(N)
x . i(x)=e(I)
Avec ces égalités, il est possible de montrer que i(e) = e grâce aux étapes suivantes :
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) . ii(e).i(e) )) 
 =A(i(e). i(e)) . ii(e).i(e) )) 
 =Ie
La transformation de l'ensemble d'égalités en système de récriture soulève plusieurs problèmes.
(x . y) . zx . (y . z)                     (A)
x . ex(N)
x . i(x)e(I)
Tout d'abord, il n'est plus possible de montrer que i(e) = e, puisqu'aucun des deux termes de l'égalité ne se réduit. La deuxième question de garantir qu'un terme ne pourra pas réduire indéfiniment, sans atteindre un résultat en un temps fini. Les propriétés correspondantes sont connues sous les noms de confluence et terminaison. La complétion est une manière de restaurer la confluence, mais le processus peut ne pas terminer, et donne seulement une procédure de semi-décision. Depuis une dizaine d'années, la recherche sur la terminaison est un domaine très actif en démonstration automatique : de nombreux critères de terminaison ont été proposés et implantés dans plusieurs outils. Depuis 2003, il y a une compétition de terminaison, qui a mis en évidence que tous les outils participants ont au moins une fois utilisé un argument non valable dans leurs démonstrations.
Nous travaillons sur les moyens de certifier certains des algorithmes à l'oeuvre dans les outils pour la récriture, et également certaines propriétés des systèmes de récriture, comme l'égalité modulo et la terminaison. Pour celà, nous développons Coccinelle, la bibliothèque Coq compagne de CiME notre boîte à outils pour la récriture. Coccinelle contient une modélisation en Coq des notions suivantes : Coccinelle peut donc être utilisée pour vérifier qu'un certificat de terminaison est valide, c'est-à-dire que lorsqu'un théorème est appliqué, toutes ses prémisses sont satisfaites.

Combinaison de procédures de décision

Le démonstrateur automatique Alt-Ergo appartient à la famille des démonstrateurs SMT (Satisfiability Modulo Theory). Il est spécialement conçu pour prouver la validité de formules issues de la preuve de programme. La syntaxe d'entrée d'Alt-Ergo est une logique du premier ordre étendue avec des théories prédéfinies et des types polymorphes. Les théories prédéfinies dans Alt-Ergo sont les suivantes:

Personnes

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

Outils

Contrats

Publications principales

[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 ]