Publications de
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.
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, .
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.