Wiki Agenda Contact English version

Publications : Xavier Urbain

Retour
[36] Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. Research Report 1560, LRI, June 2013. [ bib | full text on HAL | http | .pdf ]
[35] É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, pages 21--30, Novi Sad, Serbia, 2011. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL | http | Abstract ]
[34] É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 ]
[33] Xavier Urbain. Preuve automatique : techniques, outils et certification. Thèse d'habilitation, Université Paris-Sud 11, November 2010. [ bib ]
[32] É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 ]
[31] É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 ]
[30] Pierre Courtieu, Julien Forest, and Xavier Urbain. Certifying a Termination Criterion Based on Graphs, Without Graphs. In Otmame Aït-Mohamed, César Muñoz, and Sofiène Tahar, editors, 21th International Conference on Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science, pages 183--198. Springer, August 2008. [ bib ]
[29] Évelyne Contejean and Xavier Urbain. The A3PAT approach. In Workshop on Certified Termination WScT08, Leipzig, Germany, May 2008. [ bib ]
[28] Raúl Gutiérrez, Salvador Lucas, and Xavier Urbain. Usable rules for context-sensitive rewrite systems. In Andrei Voronkov, editor, rta08, volume 5117 of Lecture Notes in Computer Science, pages 126--141. Springer, 2008. [ bib ]
[27] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1--2):59--88, 2008. [ bib | full text on HAL | PDF | .pdf ]
[26] Évelyne Contejean, Julien Forest, and Xavier Urbain. Deep-Embedded Unification. Research Report 1547, Cédric laboratory, CNAM Paris, France, 2008. [ bib ]
[25] É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 ]
[24] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. Research Report 1185, CEDRIC, May 2007. [ bib ]
[23] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. CiME3, 2007. http://cime.lri.fr. [ bib | www: ]
[22] É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 ]
[21] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, August 2004. ACM Press. [ bib ]
[20] É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 ]
[19] Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873--897, 2004. [ bib | http ]
[18] Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1--2):89--106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ]
[17] Xavier Urbain. Modular and incremental automated termination proofs. Journal of Automated Reasoning, 32:315--355, 2004. [ bib | .ps.gz ]
[16] 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, IST VerifiCard Project, 2003. http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf. [ bib | .pdf ]
[15] Jean-Christophe Filliâtre, Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2003. http://krakatoa.lri.fr/. [ bib ]
[14] É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 ]
[13] Néstor Cataño, M. Gawlowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard project, 2003. [ bib ]
[12] Keiichirou Kusakari, Claude Marché, and Xavier Urbain. Termination of associative-commutative rewriting using dependency pairs criteria. Research Report 1304, LRI, 2002. http://www.lri.fr/~urbain/textes/rr1304.ps.gz. [ bib | .ps.gz ]
[11] Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2002. http://krakatoa.lri.fr/. [ bib ]
[10] Xavier Urbain. Modular & incremental proofs of AC-termination. Research Report 1317, LRI, 2002. [ bib | .ps.gz ]
[9] Xavier Urbain. Modular & incremental automated termination proofs. Research Report 1326, LRI, 2002. [ bib | .ps.gz ]
[8] Xavier Urbain. Approche incrémentale des preuves automatiques de terminaison. Thèse de doctorat, Université Paris-Sud, Orsay, France, October 2001. http://www.lri.fr/~urbain/textes/these.ps.gz. [ bib | .ps.gz ]
[7] Xavier Urbain. Automated incremental termination proofs for hierarchically defined term rewriting systems. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, First International Joint Conference on Automated Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence, pages 485--498, Siena, Italy, June 2001. Springer. [ bib | .ps.gz ]
[6] Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/. [ bib | http ]
[5] Évelyne Contejean, Claude Marché, Ana-Paola Tomás, and Xavier Urbain. Solving termination constraints via finite domain polynomial interpretations. Unpublished draft, International Workshop on Constraints in Computational Logics, Gif-sur-Yvette, France, September 1999. [ bib ]
[4] Claude Marché and Xavier Urbain. Termination of associative-commutative rewriting by dependency pairs. In Tobias Nipkow, editor, 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 241--255, Tsukuba, Japan, April 1998. Springer. [ bib | PDF | Abstract ]
[3] Xavier Urbain. Preuves de terminaison à l'aide de paires de dépendances. Rapport de DEA, Université Paris-Sud, Orsay, France, 1997. [ bib ]
[2] Xavier Urbain. Interprétations polynomiales et applications aux λ-calculs avec substitutions explicites. Rapport de stage de maîtrise, Université Paris-sud, 1996. [ bib | PDF | Abstract ]
[1] Francisco Duran, Salvador Lucas, Claude Marché, José Meseguer, and Xavier Urbain. Termination of membership equational programs. Submitted. [ bib ]

Retour
This page was generated by bibtex2html.