Publications

Thèses

• Xavier Urbain. Preuve automatique : techniques, outils et certification.
  Habilitation à diriger les recherches. Université Paris-Sud XI, centre d'Orsay, France, 29/11/2010.
  [pdf]
  
  
• Xavier Urbain. Approche incrémentale des preuves automatiques de terminaison.
  Thèse de doctorat. Université Paris-Sud XI, centre d'Orsay, France, 01/10/2001.
  [ps.gz]

Revues internationales

• Francisco Duran, Salvador Lucas, José Meseguer, Claude Marché et Xavier Urbain. Proving Operational Termination of Membership Equational Programs.
  Higher Order and Symbolic Computation, 21(1--2) pp 59--88, 2008.
  [pdf] [doi]
  
  
• Evelyne Contejean, Claude Marché, Ana Paula Tomás et Xavier Urbain. Mechanically proving termination using polynomial interpretations.
  Journal of Automated Reasoning, 34(4) pp 325--363, 2005.
  [pdf]   [doi]
  
  
• Xavier Urbain. Modular & Incremental Automated Termination Proofs.
  Journal of Automated Reasoning, 32(4) pp 315--355, 2004.
  [pdf] [doi]
  
  
• Claude Marché, Christine Paulin et Xavier Urbain. The Krakatoa Tool for JML/Java Program Certification.
  Journal of Logic and Algebraic Programming, 58(1--2) pp 89--106, 2004.
  [pdf] [doi]
  
  
• Claude Marché et Xavier Urbain. Modular and Incremental Proofs of AC-Termination.
  Journal of Symbolic Computation, 38(1) pp 873--897, 2004.
  [ps.gz] [doi]
  
  

Conférences

Internationales

• Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Automated Certified Proofs with CiME 3. In Manfred Schmidt-Schauß, éditeur, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), LIPIcs, Novi Sad, Serbie, 2011, à paraître.
  
  
• Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons et Xavier Urbain. A3PAT, an approach for certified automated termination proofs. In Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 10), ACM, pages 63 à 72, Madrid, Espagne, janvier 2010. [pdf] [doi]
  
  
• Pierre Courtieu, Julien Forest et Xavier Urbain. Certifying a Termination Criterion Based on Graphs, without Graphs. In César Munoz et Otmane Ait Mohamed, éditeurs, 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 08), volume 5170 de la série Lecture Notes in Computer Science, pages 183 à 198, Montréal, Canada, août 2008. [pdf]   [doi]
  
  
• Raúl Gutierrez, Salvador Lucas et Xavier Urbain. Usable rules for context-sensitive rewriting. In Andrei Voronkov, éditeur, 19th International Conference on Rewriting Techniques and Applications (RTA 08), volume 5117 de la série Lecture Notes in Computer Science, pages 126 à 141, Linz, Autriche, juin 2008. Springer-Verlag. [pdf] [doi]
  
  
• Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Certification of automated termination proofs. In Boris Konev et Frank Wolter, éditeurs, 6th International Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 de la série Lecture Notes in Artificial Intelligence, pages 148 à 162, Liverpool, Royaume-Uni, sept. 2007. Springer-Verlag. [pdf] [doi]
  
  
• Francisco Duran, Salvador Lucas, Claude Marché, José Meseguer et Xavier Urbain. Proving Termination of Membership Equational Programs. ACM SIGPLAN 2004 Symposium Partial Evaluation and Program Manipulation (PEPM 07), pages 147 à 158, Vérone, Italie, août 2004. ACM Press. [pdf] [doi]
  
  
• Xavier Urbain. Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems. In Rajeev Goré, Alexander Leitsch, et Tobias Nipkow, éditeurs, International Joint Conference on Automated Reasoning (IJCAR 01), volume 2083 de la série Lecture Notes in Artificial Intelligence, pages 485 à 498, Sienne, Italie, juin 2001. Springer-Verlag. [ps.gz] [doi]
  
  
• Claude Marché et Xavier Urbain. Termination of associative-commutative rewriting by dependency pairs. In Tobias Nipkow, éditeur, 9th International Conference on Rewriting Techniques and Applications (RTA 98), volume 1379 de la série Lecture Notes in Computer Science, pages 241 à 255, Tsukuba, Japon, avril 1998. Springer-Verlag. [ps.gz] [doi]

Nationales

• Raúl Gutiérrez, Salvador Lucas et Xavier Urbain. Towards a notion of Usable Rule for Context-Sensitive Rewrite Systems. In Ernesto Pimentel, éditeur, 7th Spanish Conference on Programming and Computer Languages (PROLE'07), Saragosse, Espagne, sept. 2007.
  

Workshops et journées

• Évelyne Contejean et Xavier Urbain. The A3PAT approach. WScT'08, Leipzig, Allemagne, juin 2008.
• Évelyne Contejean, Claude Marché, Benjamin Monate et Xavier Urbain. Proving Termination of Rewriting with CiME. WST'03, Valence, Espagne, juin 2003.
• Xavier Urbain. Proving termination automatically and incrementally. WST'01, Utrecht, Pays-Bas, mai 2001.
• Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons et Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. Sélection de [pepm10] pour présentation aux Journées nationales du GdR GPL, session LTP, Pau, France, mars 2010.

Rapports

• Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Automated Certified Proofs with CiME 3. In Technical Report 2044, Cédric, 2011. [pdf].
  
  
• Évelyne Contejean, Julien Forest, Xavier Urbain. Deep-Embedded Unification.
  Technical Report 1547, Cédric, 2008. [pdf].
  
  
• Raúl Gutiérrez, Salvador Lucas et Xavier Urbain. Towards a notion of usable rules for context-sensitive rewrite systems. Rapport de recherche DSIC II/12/07. [pdf].
  
  
• Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Certification of automated termination proofs. Rapport de recherche Cédric 1185.
  
  
• Évelyne Contejean, Claude Marché, Ana Paula Tomás et Xavier Urbain. Mechanically proving termination using polynomial interpretations. Rapport de recherche L.R.I. 1382. [ps.gz]  [pdf].
  
  
• Néstor Cataño, Marek Gawkowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch and Xavier Urbain. Logical Techniques for Applet Verification. Deliverable 5.2, VerifiCard Project, 2003.
  Available from www.verificard.org
  
  
• Xavier Urbain. Modular and Incremental Automated Termination Proofs. Rapport de recherche L.R.I. 1326. [ps.gz].
  
  
• Xavier Urbain. Modular and Incremental Proofs of AC-Termination. Rapport de recherche L.R.I. 1317. [ps.gz].
  
  
• Keiichirou Kusakari, Claude Marché et Xavier Urbain. Termination of associative-commutative rewriting using dependency pairs criteria. Rapport de recherche L.R.I. 1304. [ps.gz].