Wiki Agenda Contact Version française

Publications : Evelyne Contejean

Back
[55] Évelyne Contejean. Facettes de la preuve, Jeux de reflets entre démonstration automatique et preuve assisté. Thèse d'habilitation, Université Paris-Sud, June 2014. https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf. [ bib | full text on HAL ]
[54] Véronique Benzaken, Évelyne Contejean, and Stefania Dumbrava. A Coq formalization of the relational data model. In Z. Shao, editor, European Symposium on Programming, LNCS 8410, Lecture Notes in Computer Science, pages 189--208, Grenoble, April 2014. Springer. [ bib | full text on HAL ]
[53] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation. Logical Methods in Computer Science, 8(3):1--29, September 2012. Selected Papers of the Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany, 2011. [ bib | DOI | full text on HAL | http ]
[52] François Bobot, Sylvain Conchon, Évelyne 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 | full text on HAL ]
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 | full text on HAL | .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 | full text on HAL | 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 Évelyne 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 ]
[20] Nicolas Beldiceanu, Éric Bourreau, and Évelyne Contejean. Solving a hard vehicle routing & loading problem. In Proceedings of the Spring Meeting of the Institute for Operations Research and the Management Sciences, Montreal, April 1998. [ bib | Abstract ]
[19] Farid Ajili and Évelyne Contejean. Avoiding slack variables in the solving of linear diophantine equations and inequations. Theoretical Computer Science, 173(1):183--208, February 1997. [ bib | DOI | Abstract ]
[18] Alexandre Boudet and Évelyne Contejean. AC-unification of higher-order patterns. In Gert Smolka, editor, Principles and Practice of Constraint Programming, volume 1330 of Lecture Notes in Computer Science, pages 267--281, Linz, Austria, October 1997. Springer. [ bib | DOI | Abstract ]
[17] Évelyne Contejean, Claude Marché, and Landy Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. In Hubert Comon, editor, 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 98--112, Barcelona, Spain, June 1997. Springer. [ bib | DOI | PDF | Abstract ]
[16] Alexandre Boudet, Évelyne Contejean, and Claude Marché. AC-complete unification and its application to theorem proving. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 18--32, New Brunswick, NJ, USA, July 1996. Springer. [ bib | DOI | PDF | Abstract ]
[15] Évelyne Contejean and Claude Marché. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416--419, New Brunswick, NJ, USA, July 1996. Springer. System Description available at http://cime.lri.fr/. [ bib | DOI | PDF | http | Abstract ]
[14] Farid Ajili and Évelyne Contejean. Complete solving of linear diophantine equations and inequations without adding variables. In Ugo Montanari and Francesca Rossi, editors, Proc. First International Conference on Principles and Practice of Constraint Programming, volume 976 of Lecture Notes in Computer Science, pages 1--17, Cassis, France, September 1995. Springer. [ bib | DOI | Abstract ]
[13] Évelyne Contejean and Hervé Devie. An efficient algorithm for solving systems of diophantine equations. Information and Computation, 113(1):143--172, August 1994. [ bib | .ps.gz | Abstract ]
[12] Nicolas Beldiceanu and Évelyne Contejean. Introducing global constraints in CHIP. Journal of Mathematical and Computer Modelling, 20(12):97--123, 1994. [ bib | http | Abstract ]
[11] Alexandre Boudet and Évelyne Contejean. “Syntactic” AC-unification. In Jean-Pierre Jouannaud, editor, First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 136--151, München, Germany, September 1994. Springer. [ bib | http | Abstract ]
[10] Évelyne Contejean. Solving linear diophantine constraints incrementally. In David S. Warren, editor, Proceedings of the 10th International Conference on Logic Programming, Logic Programming, pages 532--549, Budapest, Hungary, June 1993. MIT Press. [ bib | Abstract ]
[9] Nicolas Beldiceanu, Évelyne Contejean, and Helmut Simonis. Integrating an algorithm for solving linear constraints in finite domains in the language CHIP. In Proc. 4th Workshop on Constraint Logic Programming, March 1993. [ bib | Abstract ]
[8] Évelyne Contejean. A partial solution for D-unification based on a reduction to AC1-unification. In Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors, 20th International Colloquium on Automata, Languages and Programming, volume 700 of Lecture Notes in Computer Science, pages 621--632, Lund, Sweden, July 1993. Springer. [ bib | DOI | Abstract ]
[7] Évelyne Contejean. Solving *-problems modulo distributivity by a reduction to AC1-unification. Journal of Symbolic Computation, 16(5):493--52, 1993. [ bib | DOI | Abstract ]
[6] Évelyne Contejean. Éléments pour la Décidabilité de l'Unification modulo la Distributivité. Thèse de doctorat, Université Paris-Sud, Orsay, France, April 1992. [ bib ]
[5] Alexandre Boudet and Évelyne Contejean. On n-syntactic equational theories. In Hélène Kirchner and Giorgio Levi, editors, 3th International Conference on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 446--457, Volterra, Italy, September 1992. Springer. [ bib | DOI | Abstract ]
[4] Évelyne Contejean and Hervé Devie. Résolution de systèmes linéaires d'équations diophantiennes. Comptes-Rendus de l'Académie des Sciences de Paris, 313:115--120, 1991. Série I. [ bib ]
Nous présentons ici un algorithme pour résoudre les systèmes linéaires homogènes d'équations diophantiennes de façon directe, à l'aide d'une interprétation géométrique.

[3] Alexandre Boudet, Évelyne Contejean, and Hervé Devie. A new AC-unification algorithm with a new algorithm for solving diophantine equations. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 289--299, Philadelphia, Pennsylvania, USA, June 1990. IEEE Comp. Soc. Press. [ bib | DOI | Abstract ]
[2] Évelyne Contejean and Hervé Devie. Solving systems of linear diophantine equations. In Proc. 3rd Workshop on Unification, Lambrecht, Germany. University of Kaiserslautern, June 1989. [ bib ]
[1] Évelyne Contejean. Unification associative-commutative. Mémoire de DEA , Université de Paris Sud, Orsay, 1988. [ bib ]

Back
This page was generated by bibtex2html.