Termination of Associative-Commutative Rewriting by Dependency Pairs. - Claude Marché; Xavier Urbain (RTA, 1998)

Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems. - Xavier Urbain (IJCAR, 2001)

Approche incrémentale des preuves automatiques de terminaison. (Incremental Approach for Automated Termination Proofs). - Xavier Urbain (2001)

Proving termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; José Meseguer 001; Claude Marché; Xavier Urbain (PEPM, 2004)

Modular & Incremental Automated Termination Proofs. - Xavier Urbain (J. Autom. Reason., 2004)

The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. - Claude Marché; Christine Paulin-Mohring; Xavier Urbain (J. Log. Algebraic Methods Program., 2004)

Modular and incremental proofs of AC-termination. - Claude Marché; Xavier Urbain (J. Symb. Comput., 2004)

Mechanically Proving Termination Using Polynomial Interpretations. - Evelyne Contejean; Claude Marché; Ana Paula Tomás; Xavier Urbain (J. Autom. Reason., 2005)

Certification of Automated Termination Proofs. - Evelyne Contejean; Pierre Courtieu; Julien Forest; Olivier Pons; Xavier Urbain (FroCoS, 2007)

Usable Rules for Context-Sensitive Rewrite Systems. - Raúl Gutiérrez; Salvador Lucas; Xavier Urbain (RTA, 2008)

Certifying a Termination Criterion Based on Graphs, without Graphs. - Pierre Courtieu; Julien Forest; Xavier Urbain (TPHOLs, 2008)

Proving operational termination of membership equational programs. - Francisco Durán 001; Salvador Lucas; Claude Marché; José Meseguer 001; Xavier Urbain (High. Order Symb. Comput., 2008)

A3PAT, an approach for certified automated termination proofs. - Evelyne Contejean; Andrey Paskevich; Xavier Urbain; Pierre Courtieu; Olivier Pons; Julien Forest (PEPM, 2010)

Automated Certified Proofs with CiME3. - Evelyne Contejean; Pierre Courtieu; Julien Forest; Olivier Pons; Xavier Urbain (RTA, 2011)

Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. - Cédric Auger; Zohir Bouzid; Pierre Courtieu; Sébastien Tixeuil; Xavier Urbain (SSS, 2013)

A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (CoRR, 2015)

Impossibility of gathering, a certification. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (Inf. Process. Lett., 2015)

Brief Announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (PODC, 2016)

Certified Universal Gathering in mathbb R ^2 for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (DISC, 2016)

Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (CoRR, 2016)

Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems. - Thibaut Balabonski; Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (FMICS-AVoCS, 2017)

Brief Announcement Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. - Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SSS, 2018)

Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. - Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (NETYS, 2019)

Synchronous Gathering without Multiplicity Detection: a Certified Algorithm. - Thibaut Balabonski; Amélie Delga; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (Theory Comput. Syst., 2019)

Formal Methods for Mobile Robots. - Maria Potop-Butucaru; Nathalie Sznajder; Sébastien Tixeuil; Xavier Urbain (Distributed Computing by Mobile Entities, 2019)

Computer Aided Formal Design of Swarm Robotics Algorithms. - Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SSS, 2021)

Swarms of Mobile Robots: Towards Versatility with Safety. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (Leibniz Trans. Embed. Syst., 2022)

Deterministic Color-Optimal Self-stabilizing Semi-synchronous Gathering: A Certified Algorithm. - François Bonnet 001; Quentin Bramas; Pierre Courtieu; Xavier Défago; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SIROCCO, 2025)