Xavier Thirioux

36 papers A 1B 1C 7Misc 2Journal 11Unranked 14

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. Commun. ACM Christophe Garion, Lélio Brun, Pierre-Loïc Garoche, Xavier Thirioux
2025	Misc	`conf`	BiCoq : Bigraphs Formalisation with Coq. SAC Cécile Marcon, Cyril Allignol, Célia Picard, Blair Archibald, Michele Sevegnani, Xavier Thirioux
2024	J	`jnl`	A Constraint Programming Approach for Polytopic Simulation of Ordinary Differential Equations. Acta Cybern. Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Christophe Garion, Xavier Thirioux
2023	—	`conf`	A Verified UAV Flight Plan Generator. FormaliSE Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, Xavier Thirioux
2023	J	`jnl`	Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. ACM Trans. Embed. Comput. Syst. Lélio Brun, Christophe Garion, Pierre-Loïc Garoche, Xavier Thirioux
2022	J	`jnl`	A Taxonomy of MBSE Approaches by Languages, Tools and Methods. IEEE Access Pierre de Saqui-Sannes, Rob A. Vingerhoeds, Christophe Garion, Xavier Thirioux
2021	—	`conf`	Constraint-based Verification of Formation Control. CDC Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Christophe Garion, Xavier Thirioux, Ghiles Ziat
2021	J	`jnl`	From Lustre to Simulink: Reverse Compilation for Embedded Systems Applications. ACM Trans. Cyber Phys. Syst. Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Xavier Thirioux
2021	C	`conf`	Verifying the Mathematical Library of an UAV Autopilot with Frama-C. FMICS Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, Xavier Thirioux
2020	—	`conf`	Abstract domains for constraint programming with differential equations. NSAD@SAS Ghiles Ziat, Olivier Mullier, Julien Alexandre Dit Sandretto, Christophe Garion, Alexandre Chapoutot, Xavier Thirioux
2019	J	`jnl`	Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. SIAM J. Control. Optim. Victor Magron, Pierre-Loïc Garoche, Didier Henrion, Xavier Thirioux
2019	C	`conf`	Taylor Series Revisited. ICTAC Xavier Thirioux, Alexis Maffart
2018	C	`conf`	Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. FDL Guillaume Davy, Christophe Garion, Pierre-Loïc Garoche, Pierre Roux, Xavier Thirioux
2017	B	`conf`	Automated analysis of Stateflow models. LPAR Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux
2016	J	`jnl`	Correct-by-construction model driven engineering composition operators. Formal Aspects Comput. Mounira Kezadri Hamiaz, Marc Pantel, Xavier Thirioux, Benoît Combemale
2016	—	`conf`	Hierarchical State Machines as Modular Horn Clauses. HCVS@ETAPS Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
2015	Misc	`conf`	Compilation of synchronous observers as code contracts. SAC Arnaud Dieumegard, Pierre-Loïc Garoche, Temesghen Kahsai, Alice Taillar, Xavier Thirioux
2014	C	`conf`	A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators. ICFEM Mounira Kezadri Hamiaz, Marc Pantel, Benoît Combemale, Xavier Thirioux
2014	—	`conf`	Correct-by-construction model composition: Application to the Invasive Software Composition method. FESCA Mounira Kezadri Hamiaz, Marc Pantel, Benoît Combemale, Xavier Thirioux
2014	—	`conf`	Testing-Based Compiler Validation for Synchronous Languages. NASA Formal Methods Pierre-Loïc Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux
2012	A	`conf`	Formally Defining and Iterating Infinite Models. MoDELS Benoît Combemale, Xavier Thirioux, Benoit Baudry
2011	—	`conf`	A Proof Assistant Based Formalization of MDE Components. FACS Mounira Kezadri, Benoît Combemale, Marc Pantel, Xavier Thirioux
2011	J	`jnl`	Expérimentations en Coq pour un générateur de code qualifiable. Tech. Sci. Informatiques Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
2010	—	`conf`	Use of formal methods for building qualified code generator for safer automotive systems. EDCC-CARS Nassima Izerrouken, Olivier Ssi Yan Kai, Marc Pantel, Xavier Thirioux
2009	J	`jnl`	Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. J. Softw. Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
2009	C	`conf`	Integrated Formal Approach for Qualified Critical Embedded Code Generator. FMICS Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
2009	C	`conf`	Machine-Checked Sequencer for Critical Embedded Code Generator. ICFEM Nassima Izerrouken, Marc Pantel, Xavier Thirioux
2007	—	`conf`	A Property-Driven Approach to Formal Verification of Process Models. ICEIS (Selected Papers) Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat
2007	J	`jnl`	Abstract Interpretation-based Static Safety for Actors. J. Softw. Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
2007	—	`conf`	Towards a Formal Verification of Process Model's Properties SIMPLEPDL and TOCL Case Study. ICEIS (3) Benoît Combemale, Pierre-Loïc Garoche, Xavier Crégut, Xavier Thirioux, François Vernadat
2006	J	`jnl`	Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation CoRR Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
2006	—	`conf`	Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. FMOODS Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
2003	—	`conf`	Temporal Logic Based Static Analysis for Non-uniform Behaviours. FMOODS Matthias Colin, Xavier Thirioux, Marc Pantel
2002	C	`conf`	Simple and Efficient Translation from LTL Formulas to Buchi Automata. FMICS Xavier Thirioux
2000	—	`conf`	Refinement Based Validation of an Algorithm for Detecting Distributed Termination. IPDPS Workshops Mamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec, Xavier Thirioux
1998	—	`conf`	Automatically Proving UNITY Safety Properties with Arrays and Quantifiers. IPPS/SPDP Workshops Xavier Thirioux