Publications

Thèse

• Xavier Urbain. Approche incrémentale des preuves automatiques de terminaison.
  Thèse de doctorat. Université Paris XI, centre d'Orsay, France, octobre 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.
  
  
• 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.
  [ps.gz]
  
  
• Xavier Urbain. Modular & Incremental Automated Termination Proofs.
  Journal of Automated Reasoning, 32(4) pp 315--355, 2004.
  [ps.gz]
  
  
• 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.
  [ps.gz].
  
  
• Claude Marché et Xavier Urbain. Modular and Incremental Proofs of AC-Termination.
  Journal of Symbolic Computation, 38(1) pp 873--897, 2004.
  [ps.gz].
  
  

Conférences

Internationales

• É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 (PEPM10), ACM, pages 63 à 72, Madrid, Espagne, janvier 2010.
  
  
• 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.
  
  
• Raúl Gutierrez, Salvador Lucas et Xavier Urbain. Usable rules for context-sensitive rewriting. 19th International Conference on Rewriting Techniques and Applications, Linz, Autriche, juin 2008.
  
  
• É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. [pdf]
  
  
• 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, pages 147 à 158, Vérone, Italie, août 2004. ACM Press.
  
  
• 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, volume 2083 de la série Lecture Notes in Artificial Intelligence, pages 485 à 498, Sienne, Italie, juin 2001. Éditions Springer-Verlag. [ps.gz].
  
  
• 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, volume 1379 de la série Lecture Notes in Computer Science, pages 241 à 255, Tsukuba, Japon, avril 1998. Éditions Springer-Verlag. [ps.gz].

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.
  

Rapports

• Évelyne Contejean, Julien Forest, Xavier Urbain. Deep-Embedded Unification.
  Technical Report 1547, Cédric, 2008
  
  
• 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].