Publications de Xavier THIRIOUX
Victor Magron, Pierre-Loïc Garoche, Didier Henrion, Xavier Thirioux
Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems
SIAM Journal on Control and Optimization, 2019, 57 (4), pp.2799-2820. ⟨10.1137/17M1121044⟩
Mounira Kezadri, Marc Pantel, Xavier Thirioux, Benoit Combemale
Correct-by-construction model driven engineering composition operators
Dans : Formal Aspects of Computing, Springer, Vol. 28 N. 3, p. 409-440, 2016.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
Expérimentations en Coq pour un générateur de code qualifiable
Dans : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Numéro spécial Méthodes formelles à l’analyse et la compilation, Vol. 30, N. 4/2011, p. 409-440, avril 2011.
Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
Essay on Semantics Definition in MDE. An Instrumented Approach for Model Verification.
Dans : Journal of Software (JSW), Academy Publisher, Finland, Vol. 4 N. 6, p. 943-958, novembre 2009.
Résumé Accès : http://www.academypublisher.com/ojs/index.php/jsw/article/view/0409943958
BibTeXBenoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat
A Property-Driven Approach to Formal Verification of Process Models
Dans : Enterprise Information Systems, Taylor & Francis Online, Numéro spécial LNBIP 12, ICEIS 2007, Revised Selected Papers, Vol. 12, p. 286-300, 2009.
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Abstract Interpretation-based Static Safety for Actors
Dans : Journal of Software (JSW), Academy Publisher, Finland, Vol. 2 N. 3, p. 87-98, septembre 2007.
Xavier Thirioux, Alexis Maffart
Taylor Series Revisited
International Colloquium on Theoretical Aspects of Computing (ICTAC 2019), Oct 2019, Hammamet, Tunisia. pp.335-352
Guillaume Davy, Christophe Garion, Pierre-Loïc Garoche, Pierre Roux, Xavier Thirioux
Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code
2018 Forum on specification & Design Languages (FDL), Sep 2018, Munich, France. pp.5-16, ⟨10.1109/FDL.2018.8524044⟩
Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux
Automated analysis of Stateflow models
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2017), May 2017, Maun, Botswana. pp.144-161
Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
Hierarchical State Machines as Modular Horn Clauses (regular paper)
Dans : Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016), Eindhoven, The Netherlands, 03/04/16, Vol. 219, Electronic Proceedings in Theorical Computer Science (EPTCS), p. 15-28, avril 2016.
Résumé Accès : https://doi.org/10.4204/EPTCS.219.2 – https://oatao.univ-toulouse.fr/22653/
BibTeXArnaud Dieumegard, Pierre-Loïc Garoche, Temesghen Kahsai, Alice Taillar, Xavier Thirioux
Compilation of synchronous observers as code contracts (regular paper)
Dans : Annual ACM Symposium on Applied Computing (SAC 2015), Salamanca, Spain, 13/04/15-17/04/15, ACM : Association for Computing Machinery, p. 1933-1939, avril 2015.
Accès : https://doi.org/10.1145/2695664.2695819 – https://oatao.univ-toulouse.fr/22652/
BibTeXFlorent Chevrou, Aurélie Hurault, Philippe Mauran, Meriem Ouederni, Philippe Quéinnec, Xavier Thirioux
La composition de services dans le monde asynchrone Formalisation et v ́erification en TLA+ (short paper)
Dans : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2015), Bordeaux, 09/06/15-10/06/15, Frédéric Dadeau, Pascale Le Gall (Eds.), CNRS – GDR GPL, p. 34-39, juin 2015.
Accès : http://events.femto-st.fr/sites/femto-st.fr.afadl-2015/files/content/proceedings/afadl2015.pdf – https://oatao.univ-toulouse.fr/15360/
BibTeXPierre-Loïc Garoche, Folk Howar, Temesghen Kahsai, Xavier Thirioux
Testing-Based Compiler Validation for Synchronous Languages (regular paper)
Dans : International Symposium on NASA Formal Methods (NFM 2014), Houston, Texas, 29/04/14-01/05/14, Vol. 8430, Julia M. Badger, Kristin Yvonne Rozier (Eds.), Springer, Lecture Notes in Computer Science, p. 246-251, mai 2014.
Accès : https://doi.org/10.1007/978-3-319-06200-6_19 – https://oatao.univ-toulouse.fr/22651/
BibTeXMounira Kezadri, Marc Pantel, Benoit Combemale, Xavier Thirioux
A formal framework to prove the correctness of model driven engineering composition operators (regular paper)
Dans : International Conference on Formal Engineering Methods (ICFEM 2014), Luxembourg, 03/11/14-07/11/14, Springer-Verlag, (support électronique), novembre 2014.
Mounira Kezadri, Marc Pantel, Benoit Combemale, Xavier Thirioux
Correct-by-construction model composition: Application to the Invasive Software Composition method (regular paper)
Dans : Proceedings International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2014), Grenoble, France, 12/04/14, Electronic Proceedings in Theoretical Computer Science (EPTCS), (support électronique), avril 2014.
Philippe Mauran, Philippe Quéinnec, Xavier Thirioux
Teaching Transition Systems and Formal Specifications with TLA+ (regular paper)
Dans : International Workshop on the TLA+ Method and Tools, Paris, France, 27/08/12, Kent State UNiversity, (support électronique), août 2012.
Accès : http://queinnec.perso.enseeiht.fr/publis/TLA2012.pdf
BibTeXMounira Kezadri, Benoit Combemale, Marc Pantel, Xavier Thirioux
A proof assistant based formalization of MDE components (regular paper)
Dans : Formal Aspects of Component Software (FACS 2011), Oslo, Norway, 14/09/11-16/09/11, Vol. 7253, Springer, Lecture Notes in Computer Science, (support électronique), septembre 2011.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux
Machine-Checked Sequencer for Critical Embedded Code Generator (regular paper)
Dans : Formalisation des Activités Concurrentes (FAC 2010), Toulouse, France, 31/03/10-01/04/10, ONERA, (support électronique), avril 2010.
Nassima Izerrouken, Olivier Ssi Yan Kai, Marc Pantel, Xavier Thirioux
Use of Formal Methods for Building Qualified Code Generator for Safer Automotive Systems (regular paper)
Dans : Critical Automotive applications: Robustness & Safety @ European Dependable Computing Conference (CARS@EDCC 2010), Valencia, 27/04/10-30/04/10, ACM : Association for Computing Machinery, p. 53-56, avril 2010.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux
Ordonnanceur vérifié pour un générateur de code automatique qualifiable (regular paper)
Dans : Formalisation des Activités Concurrentes (FAC 2009), Toulouse, France, 01/04/09, IRIT, (en ligne), avril 2009.
Accès : http://seminaire-verif.enseeiht.fr/FAC/2009/Papiers/32.pdf
BibTeXNassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
Integrated Formal Approach for Qualified Critical Embedded Code Generator (short paper)
Dans : International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2009), Eindhoven – The Netherlands, 02/11/09-03/11/09, Springer-Verlag, p. 199-201, 2009.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux
Machine Checked Sequencer for Critical Embedded Code Generator (regular paper)
Dans : International Conference on Formal Engineering Methods (ICFEM 2009), Rio de Janeiro, Brazil, 09/12/09-12/12/09, Springer-Verlag, p. 521-540, décembre 2009.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Martin Strecker
Certifying an Automated Code Generator Using Formal Tools: Preliminary experiments in the GeneAuto project (regular paper)
Dans : Formalisation des Activités Concurrentes (FAC 2008), Toulouse, France, 03/04/08-04/04/08, LAAS, (en ligne), avril 2008.
Accès : http://seminaire-verif.enseeiht.fr/FAC/2008/Papiers/53.pdf
BibTeXNassima Izerrouken, Xavier Thirioux, Marc Pantel, Martin Strecker
Certifying an Automated Code Generator Using Formal Tools : Preliminary Experiments in the GeneAuto Project
Dans : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 29/01/08-01/02/08, Société des Ingénieurs de l’Automobile, (support électronique), 2008.
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Spécification et Vérification par Interprétation Abstraite d’Aspects pour la Distribution
Dans : Formalisation des Activités Concurrentes (FAC 2007), Toulouse, France, 16/03/07-16/03/07, CNRS, (en ligne), mars 2007.
Xavier Thirioux, Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche
A Framework to formalise the MDE Foundations
Dans : International Workshop on Towers of Models (TOWERS 2007), Zurich, 25/06/07, Richard Paige, Jean Bézivin (Eds.), Model Driven Engineering (MDE), p. 14-30, juin 2007.
Benoit Combemale, Pierre-Loïc Garoche, Xavier Crégut, Xavier Thirioux, François Vernadat
Towards a Formal Verification of Process Model’s Properties – SimplePDL and TOCL Case Study
Dans : International Conference on Enterprise Information Systems (ICEIS 2007), Funchal, Madeira – Portugal, 12/06/07-16/06/07, INSTICC Press, p. 80-89, juin 2007 (Best paper).
Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
Expérimentation pour la définition d’une sémantique dans l’IDM
Dans : Sémantique des (meta)Modèles, Toulouse, France, 29/01/07, INPT : Institut National Polytechnique de Toulouse, p. 146-161, mars 2007.
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Static Analysis of Actors: From Type Systems to Abstract Interpretation
Dans : International Workshop on Emerging Applications of Abstract Interpretation (EAAI 2006), Vienna, Austria, 25/03/06-02/04/06, Francesco Ranzato (Eds.).
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
Dans : IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2006), Bologna, Italy, 14/06/06-16/06/06, Vol. 4037, Roberto Gorrieri, Heike Wehrheim (Eds.), Springer, LNCS , p. 78-92, juin 2006.
Matthias Colin, Marc Pantel, Xavier Thirioux
Analyse statique de la communication dans un langage d’Acteurs
Dans : Formalisation des Activités Concurrentes, Toulouse, 12/03/03-13/03/03, Mamoun Filali, Pierre Michel, François Vernadat (Eds.), Actes électroniques FERIA-SVF, p. 1-18, mars 2003.
Matthias Colin, Xavier Thirioux, Marc Pantel
Temporal logic based static analysis for non uniform behaviours
Dans : Formal Methods for Open Object-based Distributed Systems, Paris, 19/11/03-21/11/03, Springer Verlag – LNCS, p. 94-108, novembre 2003.
Simple and Efficient Translation from LTL Formulas to Buchi Automata
Dans : Workshop on Formal Methods for Industrial Critical Systems, Malaga, 12/07/02-13/07/02, Elsevier, juillet 2002.
Résumé Accès : http://www1.elsevier.com/gej-ng/31/29/23/120/53/show/Products/notes/index.htt
BibTeXMamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec, Xavier Thirioux
Refinement based validation of a distributed termination detection algorithm
Dans : International Workshop FMPPTA’2000, Cancun, 05/05/00, ., mai 2000.
Xavier Thirioux, Gérard Padiou
Etude comparative de deux techniques de preuve de programmes Unity
Dans : AFADL : Approches formelles dans l’assistance au développement de logiciels, Toulouse, ONERA-CERT, p. 177-188, mai 1997.
Xavier Thirioux, Gérard Padiou
Assistance à la preuve de programmes Unity à l’aide du démonstrateur Coq
Dans : Journées du PRC de Programmation, Orléans, .
Verifying Embedded Systems
Habilitation à diriger des recherches, Institut National Polytechnique de Toulouse, septembre 2016.
Vérification de propriétés temporelles de systèmes réactifs répartis
Thèse de doctorat, Institut National Polytechnique de Toulouse, novembre 1999.