skip to content W3C SVG

Publications

Thèses

  1. Xavier Urbain. Preuve automatique : techniques, outils et certification. Habilitation à diriger les recherches. Université Paris-Sud XI, centre d’Orsay, France, 29/11/2010. [pdf] (in English)

  2. Xavier Urbain. Approche incrémentale des preuves automatiques de terminaison. Thèse de doctorat. Université Paris-Sud XI, centre d’Orsay, France, 01/10/2001. [ps.gz] (en français)

Chapitres d’ouvrages

  1. Maria Potop-Butucaru, Nathalie Sznajder, Sébastien Tixeuil, Xavier Urbain. Formal Methods for Mobile Robots (chapter). In Paola Flocchini, Guiseppe Prencipe, Nicola Santoro, Distributed Computing by Mobile Entities, Current Research in Moving and Computing. LNCS 11340, pp 278–313, 2019. [doi]

Revues internationales

  1. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. Swarms of Mobile Robots: towards Versatility with Safety. Leibniz Transactions on Embedded Systems. 8 (2) pp 02:1–02:36, 2022. [doi]

  2. Thibaut Balabonski, Amélie Delga, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Synchronous Gathering wi1thout Multiplicity Detection: A Certified Algorithm. Theory of Computing Systems, 63 (2) pp 200–218, 2019. [doi]

  3. Béatrice Bérard, Pierre Courtieu, Laure Millet, Maria Potop-Butucaru, Lionel Rieg, Nathalie Sznajder, Sébastien Tixeuil et Xavier Urbain. Invited Paper: Formal Methods for Mobile Robots: Current Results and Open Problems. International Journal of Informatics Society, 7(3) pp 101–114, 2015. [pdf]

  4. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. Impossibility of Gathering, a Certification. Information Processing Letters, 115(3) pp 447–452, 2015. [doi]

  5. 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. [pdf] [doi]

  6. 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. [pdf] [doi]

  7. Xavier Urbain. Modular & Incremental Automated Termination Proofs. Journal of Automated Reasoning, 32(4) pp 315–355, 2004. [pdf] [doi]

  8. 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. [pdf] [doi]

  9. Claude Marché et Xavier Urbain. Modular and Incremental Proofs of AC-Termination. Journal of Symbolic Computation, 38(1) pp 873–897, 2004. [ps.gz] [doi]

Conférences

Internationales

  1. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Brief Announcement: Computer Aided Formal Design of Swarm Robotics Algorithms. In Johnen, Schiller et Schmid éd., Stabilization, Safety, and Security of Distributed Systems (SSS 2021), vol. 13046 des LNCS, pp.469-473. Novembre 2021.

  2. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In Mohamed Faouzi Atig et Alexander A. Schwarzmann, éditeurs, 7th International Conference on NETworked sYStems (NETYS 2019). Marrakech, Maroc. Juin 2019.

  3. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Brief Announcement: Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In Taisuke Izumi et Petr Kuznetsov, éditeurs, 20th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2018), volume 11201 des Lecture Notes in Computer Science, pp. 404-408. Tokyo, Japon. Novembre 2018. [doi]

  4. Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems. In Laure Petrucci, Cristina Seceleanu et Ana Cavalcanti, éditrices, Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, September 18-20, 2017, volume 10471 des Lecture Notes in Computer Science, Turin, Italie. Septembre 2017. Pages 165-181, [doi]

  5. Thibaut Balabonski, Amélie Delga, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Synchronous Gathering without Multiplicity Detection: A Certified Algorithm. In Borzoo Bonakdarpour et Franck Petit, éditeurs, 18th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2016). Lyon, France. Novembre 2016. Pages 7-19, [doi] [Version étendue dans [ToCS]]

  6. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. Certified Universal Gathering in ℝ² for Oblivious Mobile Robots. In Cyrille Gavoille et David Ilcinkas, éditeurs, 30th International Symposium on Distributed Computing (DISC 2016), volume 9888 des Lecture Notes in Computer Science, Paris, France. Septembre 2016.

  7. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. Brief Announcement: Certified Universal Gathering in ℝ² for Oblivious Mobile Robots. In Georges Giakkoupis, éditeur, 16th ACM Symposium on Principles of Distributed Computing (PODC 2016), ACM, Chicago, États-Unis. Juillet 2016. [Version étendue dans [disc16]]

  8. Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil et Xavier Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In Teruo Higashino et al., éditeurs, 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2013), volume 8255 des Lecture Notes in Computer Science, Osaka, Japon. 15 pages. Novembre 2013. [pdf] [doi]

  9. Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil et Xavier Urbain. Brief Announcement: Certified impossibility results for Byzantine-tolerant mobile robots. In Yehuda Afek, éditeur, 27th International Symposium on Distributed Computing (DISC 2013), volume 8205 des Lecture Notes in Computer Science, Jérusalem, Israël. 2 pages. Octobre 2013. [Version étendue dans [sss13]]

  10. Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Automated Certified Proofs with CiME 3. In Manfred Schmidt-Schauß, éditeur, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), LIPIcs, Novi Sad, Serbie, 2011.

  11. É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 (PEPM 10), ACM, pages 63 à 72, Madrid, Espagne, janvier 2010. [pdf] [doi]

  12. 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. [pdf] [doi]

  13. Raúl Gutierrez, Salvador Lucas et Xavier Urbain. Usable rules for context-sensitive rewriting. In Andrei Voronkov, éditeur, 19th International Conference on Rewriting Techniques and Applications (RTA 08), volume 5117 de la série Lecture Notes in Computer Science, pages 126 à 141, Linz, Autriche, juin 2008. Springer-Verlag. [pdf] [doi]

  14. É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. Springer-Verlag. [pdf] [doi]

  15. 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 (PEPM 07), pages 147 à 158, Vérone, Italie, août 2004. ACM Press. [pdf] [doi]

  16. 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 (IJCAR 01), volume 2083 de la série Lecture Notes in Artificial Intelligence, pages 485 à 498, Sienne, Italie, juin 2001. Springer-Verlag. [ps.gz] [doi]

  17. 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 (RTA 98), volume 1379 de la série Lecture Notes in Computer Science, pages 241 à 255, Tsukuba, Japon, avril 1998. Springer-Verlag. [ps.gz] [doi]

Nationales

  1. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Comment s’assurer de garder le contact (et nos distances). In AlgoTel 2021, La Rochelle , France. Sept. 2021.

  2. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Du discrètement continu au continûment discret. In AlgoTel 2020, Lyon, France. Sept. 2020.

  3. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Manuel de savoir-prouver à l’usage des roboteux et des distributeux. In Erwan Le Merre, Thomas Bégin éditeurs, AlgoTel 2019, Saint Laurent de la Cabrerisse, France, juin 2019.

  4. 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.

Workshops et journées

  1. Xavier Urbain. Towards Formal Proof for Swarms of Mobile Robots. Invité, CSTVA'17, Melbourne, Australie, août 2017.

  2. Xavier Urbain. Towards Formal Proof for Swarms of Mobile Robots. Invité, Journée Langages, Compilation, Sémantique, LIP/ÉNS Lyon, France, juin 2017.

  3. David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin et Xavier Urbain. Formal Proofs of Robustness for Watermarking Algorithms. Types’11, Bergen , Norvège, septembre 2011.

  4. Évelyne Contejean et Xavier Urbain. The A3PAT approach. WScT'08, Leipzig, Allemagne, juin 2008.

  5. Évelyne Contejean, Claude Marché, Benjamin Monate et Xavier Urbain. Proving Termination of Rewriting with CiME. WST'03, Valence, Espagne, juin 2003.

  6. Xavier Urbain. Proving termination automatically and incrementally. WST'01, Utrecht, Pays-Bas, mai 2001.

  7. Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons et Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. Sélection de pepm10 pour présentation aux Journées nationales du GdR GPL, session LTP, Pau, France, mars 2010.

Rapports

  1. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Com- puter Aided Formal Design of Swarm Robotics Algorithms. CoRR abs/2101.06966 [HAL]. 2021.

  2. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. Certified Universal Gathering in ℝ² for Oblivious Mobile Robots. Rapport de recherche, 2016. [HAL]

  3. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. Rapport de recherche LIP6, 2015. [HAL]

  4. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil et Xavier Urbain. Impossibility of Gathering, a Certification. Rapport de recherche Cédric-14-3016, 2014. [pdf]

  5. Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil et Xavier Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. Rapport de recherche L.R.I. 1560. [pdf]. [Étendu dans [SSS 13]]

  6. Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Automated Certified Proofs with CiME 3. Rapport de recherche Cédric-11-2044, 2011. [pdf]

  7. Évelyne Contejean, Julien Forest, Xavier Urbain. Deep-Embedded Unification. Rapport de recherche Cédric-08-1547, 2008. [pdf].

  8. 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].

  9. Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons et Xavier Urbain. Certification of automated termination proofs. Rapport de recherche Cédric-07-1185, 2007.

  10. É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].

  11. 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 here

  12. Xavier Urbain. Modular and Incremental Automated Termination Proofs. Rapport de recherche L.R.I. 1326. [ps.gz].

  13. Xavier Urbain. Modular and Incremental Proofs of AC-Termination. Rapport de recherche L.R.I. 1317. [ps.gz].

  14. 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].