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
CV Xavier Urbain
2001 Thèse de doctorat,
sous la direction de
Claude Marché,
Université de Paris-Sud Orsay.
Sujet : « Approche incrémentale des preuves automatiques de
terminaison ».
Novembre 1997 - août 1998 Service militaire,
Scientifique du contingent, LIX, École polytechnique.
Développement en Java
et en Camllight d'une bibliothèque graphique avec
interface de type « logo ».
1997D.E.A.
Informatique de l'Université de Paris-Sud
Orsay, mention Bien. Filière programmation :
Traitement automatique des langues (Vilnat, Sabah).
Mémoire : « Terminaison de la récriture à l'aide des paires de
dépendance » sous la responsabilité de Claude Marché, L.R.I. Orsay.
1996Maîtrise
de Mathématiques Pures, Paris-Sud Orsay :
Algèbre, (Illusie) ;
Arithmétique, (Fontaine) ;
Calculabilité et langages formels, (Comon,
Marché, Waller) ;
Systèmes vectoriels et parallèles, (Rozoy,
Beauquier, Etiemble, Laminie).
1995Licence
de Mathématiques Fondamentales, Paris-Sud Orsay.
1994 DEUG A, Paris-Sud Orsay.
1991 Baccalauréat C, lycée Poincaré,
Bar-le-Duc.
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].
Journaux
Xavier Urbain.
Modular & Incremental Automated Termination Proofs.
À paraître au Journal of Automated Reasoning.
[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. [ps.gz].
Claude Marché et Xavier Urbain.
Modular and Incremental Proofs of AC-Termination.
À paraître au Journal of Symbolic Computation.
Conférences
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
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].
Soumissions
Evelyne Contejean, Claude Marché, Ana Paula Tomás et Xavier Urbain.
Mechanically proving termination using polynomial interpretations.
Soumis.
Exposés
17 mai 2002, séminaire PROTHÉO, LORIA, Nancy, France,
Terminaison de la récriture AC, preuves modulaires et incrémentales ;
28 juin 2001, séminaire PROTHÉO, LORIA, Nancy, France,
Preuves automatiques et extensions hiérarchiques ;
22 juin 2001, « International Joint Conference on Automated
Reasoning, IJCAR », Sienne, Italie,
Automated Incremental Termination Proofs for Hierarchically
Defined Term Rewriting Systems ;