Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications : Evelyne Contejean

Back
contejean DOI ]
S0304-3r/~(96) Abstract ] 710.
 ] < ] 3jsc
[52] François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, IJCAR 2012: Proceedings of the 6th International Joint Conference on Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 67-81, Manchester, UK, June 2012. Springer. [ bib | DOI ]
This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the Alt-Ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.

[51] 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, volume 6605 of Lecture Notes in Computer Science, pages 45-59, Saarbrücken, Germany, April 2011. Springer. [ bib | DOI | .pdf | Abstract ]
[50] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In Manfred Schmidt-Schauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21-30, Novi Sad, Serbia, 2011. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. [ bib | DOI | http | Abstract ]
[49] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011. [ bib | .pdf | Abstract ]
[48] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI, Université Paris Sud, December 2010. [ bib | PDF | .pdf | Abstract ]
[47] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. In Andrei Voronkov, editor, LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, Yogyakarta, Indonesia, October 2010. (short paper). [ bib ]
[46] Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL. [ bib ]
[45] Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In John P. Gallagher and Janis Voigtländer, editors, Partial Evaluation and Program Manipulation, pages 63-72, Madrid, Spain, January 2010. ACM Press. [ bib | DOI | Abstract ]
[44] Évelyne Contejean and Xavier Urbain. The A3PAT approach. In Workshop on Certified Termination WScT08, Leipzig, Germany, May 2008. [ bib ]
[43] Évelyne Contejean. Coccinelle, a Coq library for rewriting. In Types, Torino, Italy, March 2008. [ bib ]
[42] 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 | DOI | PDF | .pdf | Abstract ]
[41] Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. CC(X): Semantical combination of congruence closure with solvable theories. In Post-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 | DOI ]
We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantical values for class representatives instead of canonized terms. Using semantical values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantical values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

[40] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. http://alt-ergo.lri.fr/. [ bib ]
[39] Sylvain Conchon and Évelyne Contejean. The Alt-Ergo automatic theorem prover. http://alt-ergo.lri.fr/, 2008. APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000. [ bib | http ]
[38] Évelyne Contejean, Julien Forest, and Xavier Urbain. Deep-Embedded Unification. Research Report 1547, Cédric laboratory, CNAM Paris, France, 2008. [ bib ]
[37] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. In Boris Konev and Frank Wolter, editors, 6th International Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 of Lecture Notes in Artificial Intelligence, pages 148-162, Liverpool,UK, September 2007. Springer. [ bib | DOI | Abstract ]
[36] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. Research Report 1185, CEDRIC, May 2007. [ bib ]
[35] Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In John Rushby and N. Shankar, editors, Proceedings of the second workshop on Automated formal methods, pages 55-59. ACM Press, 2007. [ bib | DOI | PDF | .pdf ]
Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Ergo is capable of generating proof traces for CC(X). Alternatively, Ergo can also be called interactively as a simple oracle without further verification. It is currently used to prove correctness of C and Java programs as part of the Why platform.

[34] Sylvain Conchon, Évelyne Contejean, and Johannes Kanig. CC(X): Efficiently combining equality and solvable theories without canonizers. In Sava Krstic and Albert Oliveras, editors, SMT 2007: 5th International Workshop on Satisfiability Modulo, 2007. [ bib ]
[33] Évelyne Contejean. Modelling permutations in Coq for Coccinelle. In Hubert Comon-Lundth, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 259-269. Springer, 2007. Jouannaud Festschrift. [ bib | DOI | Abstract ]
[32] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. CiME3, 2007. http://cime.lri.fr. [ bib | www: ]
[31] Évelyne Contejean and Pierre Corbineau. Reflecting proofs in first-order logic with equality. In Robert Nieuwenhuis, editor, 20th International Conference on Automated Deduction (CADE-20), volume 3632 of Lecture Notes in Artificial Intelligence, pages 7-22, Tallinn, Estonia, July 2005. Springer. [ bib | DOI | Abstract ]
[30] Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning, 34(4):325-363, 2005. [ bib | DOI | Abstract ]
[29] Évelyne Contejean. Coccinelle, 2005. http://www.lri.fr/~contejea/Coccinelle/coccinelle.html. [ bib | www: ]
[28] Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ]
[27] Évelyne Contejean. A certified AC matching algorithm. In Vincent van Oostrom, editor, 15th International Conference on Rewriting Techniques and Applications, volume 3091 of Lecture Notes in Computer Science, pages 70-84, Aachen, Germany, June 2004. Springer. [ bib | DOI | Abstract ]
[26] Évelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. Proving termination of rewriting with cime. In Albert Rubio, editor, Extended Abstracts of the 6th International Workshop on Termination, WST'03, pages 71-73, June 2003. Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain. [ bib | http ]
[25] Évelyne Contejean and Ana Paula Tomas. On Symmetries in Systems Coming from AC-Unification of Higher-Order Patterns. In Pierre Flener and Justin Pearson, editors, SymCon'01, Symmetry in Constraints, Paphos, Cyprus, December 2001. [ bib ]
[24] Alexandre Boudet and Evelyne Contejean. Combining Pattern E-unification Algorithms. In Aart Middeldorp, editor, 12th International Conference on Rewriting Techniques and Applications, volume 2051 of Lecture Notes in Computer Science, pages 63-76, Utrecht, The Netherlands, May 2001. Springer. [ bib | DOI | Abstract ]
[23] Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/. [ bib | http ]
[22] Évelyne Contejean, Antoine Coste, and Benjamin Monate. Rewriting techniques in theoretical physics. In Leo Bachmair, editor, 11th International Conference on Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 80-94, Norwich, UK, July 2000. Springer. [ bib | DOI | Abstract ]
[21] Alexandre Boudet and Evelyne Contejean. About the Confluence of Equational Pattern Rewrite Systems. In C. and H. Kirchner, editors, 15th International Conference on Automated Deduction, volume 1421 of Lecture Notes in Computer Science, pages 88-102, Lindau, Germany, July 1998. Springer. [ bib | DOI | Abstract ]
[bib |  |implicejeaon'="cone Contejean. About the Confluence of Equational Pattern RewriS"http:/nteu/~dvehiy r Sytp:/& loadIn bib | .ps.gz ] < ]
[47] Évelyne CFariNotjiliyne Contejean. About the Confluence of Equational Pattern Rewritvoe the slackmberie.lrith uni="http:/iliforms. dioe Erytpib.he Kure Notpi Ku):325-3Tunysb.edu/~ July 2000. Springer. [173(1):/em-208, Febrn_bitml#mt">bib ]
[21] Évelyne Contejean, Evelyne Contejean. About the Confluence of Equational Pattern RewritC.score.is.tsuilihstin Pww-lsipditors, St van Oostrom, edsl">Ma Inr> ~smolk of G theSmolk on Rewriting TecPt98ciplture NoPerifi and H [ , pages 259-269Springer, 2007. Jouannaud Festschriftb.ht67-2bib | DOI | Abstract ] [26] Évelyne Contejean. A certified AC matching r/~marche/">Claude Marché, Bernhard Gramlich, a>-Lundth, bib | DOI | Abstract, py s/10.#mtgn="tophon/publis/conchon-smt08.pdf">.pdf lix.pol10.#mtign="top"> [21] Évelyne Contejean, Evel Contejean, Mohamed IgueMebsout. The Alt-Ergo automaix.polytechnique.fr/Labo/writC.is imple score.is.tsue Nott clas in Coen prochttp://al08. [ ut. The Alt-ErmpMa Inmpgnr> ~hininHacald Ganz98cadhne/ Rewriting Tecramming, Artificial Intellig, volume 1833 of Lecture Notes in Computer Science, pages 80-94, Norwich, UK, July 2000. Springer. [ 18-3occNew BrunswickccNJ, USA_bib.html#6tudet98cade">bib | DOI | Abstractlix.pol>, py s/10.#6tgn="tophon/publis/conchon-smt08.pdf">.pdf lix.pol10.#6lign="top"> [26] Évelyne Contejean and Ana Paula Tomas. r/~iguer/">Mohamed IgeMebsout. The Alt-Ergo automaix.polytechnique.fr/Labo/wrip://:ef="http://www.cs.mhttp://www [ ut. The Alt-ErmpMa Inmpgnr> ~hininHacald Ganz98cadhne/ Rewriting Tecramming, Artificial Intellig, volume 1833 of Lecture Notes in Computer Science, pages 80-94, Norwich, UK, July 2000. Springer. [ 416-419ccNew BrunswickccNJ, USA_bib.html#6tboudet01rta">15t D ps.tsue/cime.lri.fr/. [ bib | DOI | Abstractlix.pol>, py s/html-10.#6tgn="tophon/publis/conchon-smt08.pdf">.p valign="top"> Abstractlix.polhtml-10.#6tign="top"> [47] AlexandreFariNotjiliyne Contejean. About the Confluence of Equational Pattern RewriCs imple ="http:/iliforms. dioe Erytpihe Kure Notpi Ku used to ad the berie.lri [ ut. The Alt-Erdil">Mpi.it/~ugo/ugotign="tUgoS ph&anerid IgeMebs#contesca Rces hop on Automated fo. Fp://em>, pages 1-5, 2008. [ Voigt98ciplture NoPerifi and H [ bib | DOI | httpl">Abstract ] [26] Evelyne Contejean, Claude Mationalervé D vime.hAn. Our combination of="http:/=r Pat supioe Erytpihe Ku):325-3Itly used fories. ure Nonger. [113(1):/43-1[2,_bugusttml#4rr">bib | DOItpef="httpLRIl>, py s/hw.lri.fr/ic#4rgn="top"> Abstract ] [bib | 4jmcne 1tp://www.lri.fr/~contejea/">Évelyne Crico witBa> |yne Contejean. About the Confluence of Equational Pattern Rewri, prw.cctp:/Shostak [ bib | DOI ]
0895-7177(94)90.fr/contejea/publis/2011rta/abstract.html">Abstract ]
[48] Alexandre Boudet and Evelyne Contejean. About the Confluence of Equational Pattern Rewri“Syh&aifi ”itC.score.is.tsh/">Bernhard Gramlich, min Monate. RewritinJter-ymCon'._bib.html"httter-ymCon'n_bib.htmlhne/ Rewriting TecFp://ming, Artificial Intelligence aC[ bib | DOI | Abstract ]
[48] Évelyne Contejean, , pages 71-7008. [ Voind Rea. l.lri.fr/lr Scind Rea. l.lri.frschriftb.h532www9ccBudapest, Hungarytejrsidml#3. MITjean10pepm">bib | .ps.gz ] < ] [bib | 3">tp://www.lri.fr/~contejea/">Évelyne Crico witBa> |imontejean, Mohamed IgueMebsHelmto Simonii [&nbis capaories combination of="http:/forms. [ bib | www: ] [bibÉvelyne Contejean, AC1.score.is.tsh/">Be"httzejhhregorksRolf Karlsraintn of vEryers, lsraintem>, Pau, Franceuction (CADE-20)lloqu),ture Noa> wwurifure NoPe l.lri.fr/lr Science, pages 259-269Springer, 2007. Jouannaud Festschrift.i.fr63occ>Cla_bewed n nce,b.html#3tudet98cade">bib | DOI | Abstract ] [bibÉvelyne Contejean. A certified AC matching r/~marche/">Claude MawriS"http:/*-a hd ths implieddinbs=buedv_bibnd i rure Notes

eries< Fest1.score.is.tsh/"25-363, 2005. [Sn ordtors ure Nonger. [16(5):49/ww2,h1l#3.r">bib | DOI | Abstract ]

[bibtp://www.lri.fr/~contejea/">Évelyne Contejean, Claude Mawri25-3Éléso es p3, i// Décidjean_bé dni/'re Flener aX frmplied// Dinbs=buedv_bé//www [&Thès enhdoctf="c href="contejean_b-b.htmOrsayml#contejebib.hb.h1l#2.r">bib | [24] Évelyne Contejean and Ana Ptp://www.lri.fr/~contejea/">Evelyne Contejean. About the Confluence of Equational Pattern RewriOWorkshonger.-syh&aifi he K005toronkov/">Andrei Voronkov, edors, Rewriting, Computation and Prooies. ihreio Lev hop on Automate303, pages 71-7008. [ VoiAlgebsp;h Innd Rea. l.lri.fr/lr Scicience erie259-269Springer, 2007. Jouannaud Festschrift.446-457, Vm on orks.html#tejean_bib.ht1l#2.udet01rta">bib | DOI | Abstract ] [bibtp://www.lri.fr/~contejea/">Évelyne Contejean and Claude Mationalervé D vime.hRé="hued fodni=r èmft.foréair GPL'é Ku dioe Eryteualiwri25-32007ing-Rendus dni/'Académi ens9uly 199m dniean_b8. Spring313:115-120,h1l#l#boSénko I.r">bib | ncomponeejeài/'anbspd'rsi 4. [&nbée Notgéomébs=>. ign="top"> [40] doi.orr0dto="htp://www.lri.fr/~contejea/">Évelyne Contejean, Evel Contejean, Mohamed IgueMebslervé D vime.hAterprtC.score.is.tsucombinatioc.es/ogram vombination of="http: dioe Erytpihe Ku):3 Worksho Satisfiability MFifes/Annuia, EEEoCos 07),nd Rea, UK, July 2000. Springer. [ 289-299, Philadelph="coPeuascontean_bUSA_bibpib.h1l#0., EEEo Jul.ud S. ean10pepm">bib | DOI | Abstract ] [bibtp://www.lri.fr/~contejea/">Évelyne Contejean, Antoine Coste, and Claude Mationalervé D vime.hS"http:/=r Pat suforms. dioe Erytpihe Ku):3 Worksho S. 3rd73, June 2003re Flener a> mbnbsp;bib | [24] tp://www.lri.fr/~contejea/">Évelyne Contejean and Pierre Corbineau. RefEquational Pattern Rewrire Flener annteoci as a.is tp://wvme.hMémompo dniDEA href="contejdniean_b b.htmOrsaymlml88rr">bib ]
and//alalef="httpti and Pierre Corbfilli atpti >Év2ign=/">Év2ign=n Rewrn="top"btex/div>ex/div>exdiv id="fogn=ss="©html#-tml2a. Via,- D et0r/. [ . [ CssT P Evel Cnd ontejean and s P darkf inEvelex/div>ex/