Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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].
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.
Evelyne Contejean, Claude Marché, Ana Paula Tomás et Xavier Urbain.
Mechanically proving termination using polynomial interpretations.
À paraître au Journal of Automated Reasoning.
Conférences
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].
Rapports
Evelyne 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].