Automatically Proving UNITY Safety Properties with Arrays and Quantifiers. - Xavier Thirioux (IPPS/SPDP Workshops, 1998)

Refinement Based Validation of an Algorithm for Detecting Distributed Termination. - Mamoun Filali; Philippe Mauran; Gérard Padiou; Philippe Quéinnec; Xavier Thirioux (IPDPS Workshops, 2000)

Simple and Efficient Translation from LTL Formulas to Buchi Automata. - Xavier Thirioux (FMICS, 2002)

Temporal Logic Based Static Analysis for Non-uniform Behaviours. - Matthias Colin; Xavier Thirioux; Marc Pantel (FMOODS, 2003)

Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. - Pierre-Loïc Garoche; Marc Pantel; Xavier Thirioux (FMOODS, 2006)

A Property-Driven Approach to Formal Verification of Process Models. - Benoît Combemale; Xavier Crégut; Pierre-Loïc Garoche; Xavier Thirioux; François Vernadat 001 (ICEIS (Selected Papers), 2007)

Towards a Formal Verification of Process Model's Properties SIMPLEPDL and TOCL Case Study. - Benoît Combemale; Pierre-Loïc Garoche; Xavier Crégut; Xavier Thirioux; François Vernadat 001 (ICEIS (3), 2007)

Abstract Interpretation-based Static Safety for Actors. - Pierre-Loïc Garoche; Marc Pantel; Xavier Thirioux (J. Softw., 2007)

Integrated Formal Approach for Qualified Critical Embedded Code Generator. - Nassima Izerrouken; Marc Pantel; Xavier Thirioux; Olivier Ssi Yan Kai (FMICS, 2009)

Machine-Checked Sequencer for Critical Embedded Code Generator. - Nassima Izerrouken; Marc Pantel; Xavier Thirioux (ICFEM, 2009)

Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. - Benoît Combemale; Xavier Crégut; Pierre-Loïc Garoche; Xavier Thirioux (J. Softw., 2009)

Use of formal methods for building qualified code generator for safer automotive systems. - Nassima Izerrouken; Olivier Ssi Yan Kai; Marc Pantel; Xavier Thirioux (EDCC-CARS, 2010)

A Proof Assistant Based Formalization of MDE Components. - Mounira Kezadri; Benoît Combemale; Marc Pantel; Xavier Thirioux (FACS, 2011)

Expérimentations en Coq pour un générateur de code qualifiable. - Nassima Izerrouken; Marc Pantel; Xavier Thirioux; Olivier Ssi Yan Kai (Tech. Sci. Informatiques, 2011)

Formally Defining and Iterating Infinite Models. - Benoît Combemale; Xavier Thirioux; Benoit Baudry (MoDELS, 2012)

A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators. - Mounira Kezadri Hamiaz; Marc Pantel; Benoît Combemale; Xavier Thirioux (ICFEM, 2014)

Testing-Based Compiler Validation for Synchronous Languages. - Pierre-Loïc Garoche; Falk Howar; Temesghen Kahsai; Xavier Thirioux (NASA Formal Methods, 2014)

Correct-by-construction model composition: Application to the Invasive Software Composition method. - Mounira Kezadri Hamiaz; Marc Pantel; Benoît Combemale; Xavier Thirioux (FESCA, 2014)

Compilation of synchronous observers as code contracts. - Arnaud Dieumegard; Pierre-Loïc Garoche; Temesghen Kahsai; Alice Taillar; Xavier Thirioux (SAC, 2015)

Hierarchical State Machines as Modular Horn Clauses. - Pierre-Loïc Garoche; Temesghen Kahsai; Xavier Thirioux (HCVS@ETAPS, 2016)

Correct-by-construction model driven engineering composition operators. - Mounira Kezadri Hamiaz; Marc Pantel; Xavier Thirioux; Benoît Combemale (Formal Aspects Comput., 2016)

Automated analysis of Stateflow models. - Hamza Bourbouh; Pierre-Loïc Garoche; Christophe Garion; Arie Gurfinkel; Temesghen Kahsai; Xavier Thirioux (LPAR, 2017)

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. - Guillaume Davy; Christophe Garion; Pierre-Loïc Garoche; Pierre Roux 001; Xavier Thirioux (FDL, 2018)

Taylor Series Revisited. - Xavier Thirioux; Alexis Maffart (ICTAC, 2019)

Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. - Victor Magron; Pierre-Loïc Garoche; Didier Henrion; Xavier Thirioux (SIAM J. Control. Optim., 2019)

Abstract domains for constraint programming with differential equations. - Ghiles Ziat; Olivier Mullier; Julien Alexandre Dit Sandretto; Christophe Garion; Alexandre Chapoutot; Xavier Thirioux (NSAD@SAS, 2020)

Constraint-based Verification of Formation Control. - Julien Alexandre Dit Sandretto; Alexandre Chapoutot; Christophe Garion; Xavier Thirioux; Ghiles Ziat (CDC, 2021)

Verifying the Mathematical Library of an UAV Autopilot with Frama-C. - Baptiste Pollien; Christophe Garion; Gautier Hattenberger; Pierre Roux 001; Xavier Thirioux (FMICS, 2021)

From Lustre to Simulink: Reverse Compilation for Embedded Systems Applications. - Hamza Bourbouh; Pierre-Loïc Garoche; Christophe Garion; Xavier Thirioux (ACM Trans. Cyber Phys. Syst., 2021)

A Taxonomy of MBSE Approaches by Languages, Tools and Methods. - Pierre de Saqui-Sannes; Rob A. Vingerhoeds; Christophe Garion; Xavier Thirioux (IEEE Access, 2022)

A Verified UAV Flight Plan Generator. - Baptiste Pollien; Christophe Garion; Gautier Hattenberger; Pierre Roux 001; Xavier Thirioux (FormaliSE, 2023)

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. - Lélio Brun; Christophe Garion; Pierre-Loïc Garoche; Xavier Thirioux (ACM Trans. Embed. Comput. Syst., 2023)

A Constraint Programming Approach for Polytopic Simulation of Ordinary Differential Equations. - Julien Alexandre Dit Sandretto; Alexandre Chapoutot; Christophe Garion; Xavier Thirioux (Acta Cybern., 2024)

BiCoq : Bigraphs Formalisation with Coq. - Cécile Marcon; Cyril Allignol; Célia Picard; Blair Archibald; Michele Sevegnani; Xavier Thirioux (SAC, 2025)