Normalized Types. - Pierre Courtieu (CSL, 2001)

Représentation d'algèbres non libres en théorie des types. (Representation of Non Free Algebras in Type Theory). - Pierre Courtieu (2001)

Tool-Assisted Specification and Verification of the JavaCard Platform. - Gilles Barthe; Pierre Courtieu; Guillaume Dufay; Simão Melo de Sousa (AMAST, 2002)

Proving Self-Stabilization with a Proof Assistant. - Pierre Courtieu (IPDPS, 2002)

Efficient Reasoning about Executable Specifications in Coq. - Gilles Barthe; Pierre Courtieu (TPHOLs, 2002)

Tool-Assisted Specification and Verification of Typed Low-Level Languages. - Gilles Barthe; Pierre Courtieu; Guillaume Dufay; Simão Melo de Sousa (J. Autom. Reason., 2005)

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

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

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

Improved Matrix Interpretation. - Pierre Courtieu; Gladys Gbedo; Olivier Pons (SOFSEM, 2010)

Structural Analysis of Narratives with the Coq Proof Assistant. - Anne-Gwenn Bosser; Pierre Courtieu; Julien Forest; Marc Cavazza (ITP, 2011)

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

Maximal and Compositional Pattern-Based Loop Invariants. - Maria-Virginia Aponte; Pierre Courtieu; Yannick Moy; Marc Sango (FM, 2012)

Towards Provably Robust Watermarking. - David Baelde; Pierre Courtieu; David Gross-Amblard; Christine Paulin-Mohring (ITP, 2012)

Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. - Pierre Courtieu; Maria-Virginia Aponte; Tristan Crolard; Zhi Zhang; Robby; Jason Belt; John Hatcliff; Jérôme Guitton; Trevor Jennings (HILT, 2013)

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)

Focused Certification of an Industrial Compilation and Static Verification Toolchain. - Zhi Zhang; Robby; John Hatcliff; Yannick Moy; Pierre Courtieu (SEFM, 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)

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)