Xavier URBAIN

Situation

• Post-doc INRIA, Projet LogiCal, Thème : « Vérification de code JavaCard » (Verificard).

Implications

• Membre du projet européen Verificard ;
• Membre de la jeune équipe CiME (Projet ATIP C.N.R.S. démarré en novembre 2001) ;
• Membre d'un projet d'action bilatérale C.N.R.S./U.I.U.C.

Cursus

• 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 ».
  
  *** Thèse distinguée par l'AFIT en 2002. ***
  
  
• 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 ».
  
  
• 1997 D.E.A. Informatique de l'Université de Paris-Sud Orsay, mention Bien.
  Filière programmation :
  • Récriture (Jouannaud, Puel) ;
  • Spécifications formelles (Bernot, Le Gall) ;
  • Bases de données à objets (Delobel, Benzaken) ;
  • Interaction homme/machine (Beaudouin-Lafon, MacKay) ;
  • 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.
• 1996 Maî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).
• 1995 Licence 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 ;
• 21 mai 2001, « Fifth International Workshop on Termination, WST'01 », Utrecht, Pays-bas,
  Proving termination automatically and incrementally.
  Résumé.

Colloques et écoles

• 22 - 24 mai 2001, « 12^th international conference on Rewriting Techniques and Applications, RTA'01 », Utrecht, Pays-bas 
• 20 - 21 mai 2001, « Fifth International Workshop on Termination, WST'01 », Utrecht, Pays-bas ;
• 5 - 8 septembre 1999, école d'été CCL, Gif-sur-Yvette, France, « Constraints in Computational Logics, CCL'99 » ;
• 2 - 4 juillet 1999, « 10^th international conference on Rewriting Techniques and Applications, RTA'99 », FLoC'99, Trente, Italie ;
• 7 - 10 juillet 1999, « 16^th international conference on Automated Deduction, CADE-16 », FLoC'99, Trente, Italie ;
• 10 - 12 mai 1999, « Fourth International Workshop on Termination, WST'99 », Dagstuhl, Allemagne ;
• Août 1997, école d'été de l'I.P.A., Mierlo, Pays-Bas, « Summer school on syntactic and computational methods » ;
• 21 - 23 mai 1997, « Third International Workshop on Termination », Utrecht, Pays-Bas.

Stages

• Mars - septembre 1997, stage de D.E.A., avec Claude Marché, L.R.I. Orsay, « Terminaison de la récriture à l'aide des paires de dépendance » ;
• Juillet - août 1996, avec Claude Marché, L.R.I. Orsay, « Ordres polynomiaux et lambda-calculs avec substitutions explicites ».

Enseignement

• Depuis octobre 1998 Moniteur du rectorat de Versailles.
  • Premier semestre 2000-2001 Principes d'interprétation des langages (P.I.L.), T.D. et T.P., D.E.U.G. S3-MIAS de Paris-Sud, Orsay ;
  • Second semestre 2000-2001 Logique et matériel, T.D. et T.P., D.E.U.G. S4-MIAS de Paris-Sud, Orsay ;
    
    
  • Premier semestre 1999-2000 Principes d'interprétation des langages (P.I.L.), T.D. et T.P., D.E.U.G. S3-MIAS de Paris-Sud, Orsay ;
  • Second semestre 1999-2000 Logique et matériel, T.D. et T.P., D.E.U.G. S4-MIAS de Paris-Sud, Orsay ;
    
    
  • Premier semestre 1998-1999 T.E.R. de compilation de la maîtrise d'informatique de Paris-Sud, Orsay ;
  • Second semestre 1998-1999 Approche fonctionnelle, T.P. et étude de cas, D.E.U.G. S2-MIAS de Paris-Sud, Orsay.

Langues

• Anglais courant, notions de russe.

Loisirs

• Cuisine, cyclisme et course à pied.