Responsable : Philippe QUéINNEC
L’équipe ACADIE (Assistance à la Certification d’Applications DIstribuées et Embarquées) étudie le développement et la vérification de systèmes logiciels critiques pour lesquels il est nécessaire d’exhiber un certificat de correction. L’essence d’un tel certificat est une preuve mathématique de correction. L’équipe ACADIE étudie comment élaborer un tel certificat à trois niveaux :
- Au niveau fondamental, les concepts de preuve et de calcul sont étudiés. Le cadre formel de la théorie des types et la théorie des catégories est considéré.
- Au niveau méthode, nous étudions les concepts structurants nécessaires pour faciliter la production de preuves de correction. De plus, nous nous intéressons aux processus de production de logiciels corrects par construction. Nous considérons le développement de logiciels critiques.
- Au niveau applicatif, nous étudions les systèmes temps réel distribués et en particulier, les systèmes embarqués critiques. Notre objectif est de comprendre les abstractions principales et les processus de développement de ce domaine applicatif, afin de fournir une assistance à la vérification de systèmes distribués critiques.
L’équipe ACADIE est structurée en trois groupes :
- Théorie des types et théorie des catégories
- Développement de logiciels critiques
- Vérification de systèmes distribués critiques
Compétences
personnel de l’équipe
- Yamine AIT AMEURProfesseur – INPT
- Jean-Paul BODEVEIXProfesseur – UPS
- Xavier CRéGUTMaître de Conférences – INPT
- Mamoun FILALIChargé de Recherche – CNRS
- Aurélie HURAULTMaître de Conférences – INPT
- Erik MARTIN-DORELMaître de Conférences – UPS
- Ralph MATTHESChargé de Recherche – CNRS
- Philippe MAURANMaître de Conférences – INPT
- Benoit MORGANMaître de Conférences – INPT
- Meriem OUEDERNIMaître de Conférences – INPT
- Marc PANTELMaître de Conférences – INPT
- Philippe QUéINNECProfesseur – INPT
- Jean-Baptiste RACLETMaître de Conférences – UPS
- Neeraj SINGHMaître de Conférences – INPT
- Jan-Georg SMAUSProfesseur – UPS
- Sergei SOLOVIEVProfesseur – UPS
- Martin STRECKERMaître de Conférences – UPS
- Xavier THIRIOUXMaître de Conférences – INPT
- Sarah BENYAGOUBStage doctoral
- Jonathan CERTESDoctorant IRIT – UPS
- Nassima DJEMAStage doctoral
- Guillaume DUPONTDoctorant IRIT – INPT
- Alexandra HALCHINDoctorant IRIT – INPT
- Maksim KALAMEYETSDoctorant IRIT – UPS
- Alexis MAFFARTDoctorant IRIT – INPT
- Ian MALAKHOVSKIDoctorant IRIT – UPS
- Ismail MENDILDoctorant IRIT – INPT
- Mathieu MONTINDoctorant IRIT – INPT
- Pierre POMERET-COQUOTMaster 2 IRIT – UPS
- Matthieu ROYCollaborateur extérieur
- Adam SHIMIDoctorant IRIT – INPT
- Zhibin YANGChercheur invité
- Christelle CHAUDETMaître de Conférences – UPS
publications de l’équipe
Sergei Soloviev, Nadezda Orlova
Logic and logicians in Russia before 1917: Living in a wider world
Dans : Historia Mathematica, Elsevier, Vol. 46, p. 38-55, février 2019.
Résumé Accès : https://www.sciencedirect.com/science/article/pii/S0315086018300612 – https://doi.org/10.1016/j.hm.2018.05.002 – https://oatao.univ-toulouse.fr/26301/
BibTeXSergei Soloviev, Ian Malakhovski
Automorphisms of Types and Their Applications.
Dans : Journal of Mathematical Sciences, Springer, Vol. 240 N. 5, p. 692-706, août 2019.
Fei Wang, Zhibin Yang, Zhi-Qiu Huang, Cheng-Wei Liu, Yong Zhou, Jean-Paul Bodeveix, Mamoun Filali
An Approach to Generate the Traceability Between Restricted Natural Language Requirements and AADL Models
Dans : IEEE Transactions on Reliability, IEEE : Institute of Electrical and Electronics Engineers, Vol. 1 N. 1, p. 1-20, septembre 2019.
Résumé Accès : http://doi.org/10.1109/TR.2019.2936072 – https://oatao.univ-toulouse.fr/25027/
BibTeXJosé Espírito Santo, Ralph Matthes, Luís Pinto
Decidability of several concepts of finiteness for simple types
Dans : Fundamenta Informaticae, IOS Press, Vol. 170 N. 1-3, p. 111-138, octobre 2019.
Résumé Accès : https://doi.org/10.3233/FI-2019-1857 – https://hal.archives-ouvertes.fr/hal-02119503v1
BibTeXFlorent Chevrou, Aurélie Hurault, Philippe Quéinnec
A Modular Framework for Verifying Versatile Distributed Systems
Dans : Journal of Logical and Algebraic Methods in Programming, Elsevier, Vol. 108, p. 24-46, novembre 2019.
Accès : http://pardi.enseeiht.fr/Papers/jlamp.pdf – https://oatao.univ-toulouse.fr/24923/
BibTeXJosé Espírito Santo, Ralph Matthes, Luís Pinto
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 29, p. 1092-1124, septembre 2019.
Résumé Accès : https://doi.org/10.1017/S0960129518000099 – https://hal.archives-ouvertes.fr/hal-02360678v1
BibTeXAutomorphisms of Types in Certain Type Theories and Representation of Finite Groups
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 29 N. 4, p. 511-551, avril 2019.
Résumé Accès : https://doi.org/10.1017/S0960129518000129 – https://oatao.univ-toulouse.fr/26149/
BibTeXBenedikt Ahrens, Ralph Matthes, Anders Mörtberg
From signatures to monads in UniMath
Dans : Journal of Automated Reasoning, Springer-Verlag, Heidelberg, Allemagne, Vol. 63 N. 2, p. 285-318, août 2019.
Résumé Accès : https://doi.org/10.1007/s10817-018-9474-4
BibTeXLynda Ait Oubelli, Yamine Ait Ameur, Judicael Bedouet, Romain Kevarc, Benoit Chausserie-Lapree, Beatrice Larzul
A scalable model based approach for data model evolution: Application to space missions data models
Dans : Computer Languages, Systems and Structures, Elsevier, Vol. 54, p. 358-385, 2018.
Abdelkrim Chebieb, Yamine Ait Ameur
A formal model for plastic human computer interfaces
Dans : Frontiers of Computer Science, Springer, Vol. 12 N. 2, p. 351-375, 2018.
Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali
Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL
Dans : Frontiers of Computer Science, Springer, Numéro spécial Semantic-focused Modelling of Embedded Architectures, Vol. 13, N. 4, p. 715-734, août 2019.
Accès : https://doi.org/10.1007/s11704-017-6485-y – https://oatao.univ-toulouse.fr/24993/
BibTeXStudes of Hilbert’s Epsilon Operator in the USSR
Dans : The IfCoLog Journal of Logics and their Applications, College Publications, UK, Numéro spécial Hilbert’s epsilon and tau in Logics, Informatics and Linguistics, Vol. 4, N. 2, p. 427-437, avril 2017.
Résumé Accès : http://collegepublications.co.uk/contents/ifcolog00011.pdf – https://oatao.univ-toulouse.fr/19099/
BibTeXYang Zhibin, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu
Towards a verified compiler prototype for the synchronous language SIGNAL
Dans : Frontiers of Computer Science, Springer, Vol. 10, N. 1, p. 37-53, février 2016.
Zhibin Yang, Kai Hu, Yongwang Zhao, Dianfu Ma, Jean-Paul Bodeveix
AADL Model Verification by Translating into TASM
Dans : Journal of Software, Institute of Software Chinese Academy of Science (ISCAS), China, Vol. 26, N. 2, p. 1-20, février 2015.
Aurélie Hurault, Marc Pantel, Michel Daydé
Composition automatique de services de calcul – Utilisation des spécifications algébriques pour décrire la fonctionnalité des services
Dans : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Numéro spécial La composition d’objets, de composants et de services, Vol. 30, N. 6/2011, p. 685-710, juin 2011.
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.
Zhibin Yang, Lei Pi, Kai Hu, Zong-Hua Gu, Dianfu Ma
AADL: an Architecture Design and Analysis Language for Complex Embedded Real-time Systems
Dans : Journal of Software, Institute of Software Chinese Academy of Science (ISCAS), China, Vol. 21, N. 5, p. 899-915, mai 2010.
Accès : http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3700&flag=1
BibTeXAngel Garcia, Benoit Combemale, Xavier Crégut, Jérôme Vandeur
TopPROCESS : vers une ingénierie des procédés dirigée par les modèles
Dans : Revue de l’Electricité et de l’Electronique (REE), Société de l’Electricité, de l’Electronique et des Technologies de l’Information et de la Communication (SEE), Paris, Vol. 2009, N. 2, p. 31-37, février 2009.
Odile Nasr, Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali
Spécification et vérification d’un ordonnanceur en B via les automates temporisés
Dans : L’Objet, Hermès Science, Numéro spécial Composants, services et aspects techniques et outils pour la vérification, Vol. 14, N. 4, p. 43-72, décembre 2008.
Olga Antonova, Sergei Soloviev
Le test de Turing et la question d’une definition de la realite virtuelle
Dans : Logiko-philosophskie shtudii. (Etudes logiko-philosophiques), Universite d’Etat de St. Petersbourg, Russia, Vol. 5, p. 50-67, 2008.
Ladjel Bellatreche, Yamine Ait Ameur, George Angelos Papadopoulos
Models and Data Engineering
Dans : Future Generation Computer Systems, Elsevier, Vol. 70, 2017.
Ladjel Bellatreche, Yamine Ait Ameur, George Angelos Papadopoulos
Models and Data Engineering
Dans : Future Generation Computer Systems, Elsevier, Vol. 68, 2017.
David Baelde, Arnaud Carayol, Ralph Matthes, Igor Walukiewicz
Fixed Points in Computer Science (FICS) 2013
Dans : Fundamenta Informaticae, IOS Press, Vol. 150 N. 3-4, mars 2017.
Yamine Ait Ameur, Klaus-Dieter Schewe
Introduction to the ABZ 2014 special issue
Dans : Science of Computer Programming, Elsevier, Vol. 131, 2016.
Ladjel Bellatreche, Yamine Ait Ameur, Anne Monceaux
Editorial
Dans : Computers in Industry, Elsevier, Vol. 65 N. 9, 2014.
Special Issue « Sixth Workshop on Fixed Points in Computer Science, FICS 2009 »
Dans : RAIRO – Theoretical Informatics and Applications, EDP Sciences, Vol. 47 N. 1, 2013.
Ralph Matthes, Sergei Soloviev
CAMCAD ’09 Commutativity of Algebraic Diagrams
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 22 N. 6, décembre 2012.
Accès : http://journals.cambridge.org/action/displayIssue?jid=MSC&volumeId=22&seriesId=0&issueId=06
BibTeXRalph Matthes, Sergei Soloviev
Isomorphism of types and invertibility of lambda terms
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 18, août 2008.
Sergei Soloviev, Roberto Di Cosmo
Isomorphism of Types
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 15 N. 5, octobre 2005.
Jean-Paul Arcangeli, Mamoun Filali, Abdelkader Hameurlain, Gérard Padiou
Les environnements d’exécution répartie
Dans : Calculateurs Parallèles, Réseaux et Systèmes Répartis, HERMES, 8, quai du Marche-Neuf 75004 Paris France, Vol. 10, 5, 1998.
K-set agreement bounds in round-based models through combinatorial topology (regular paper)
Dans : ACM Symposium on Principles of Distributed Computing (PODC 2020), Salerno, Italy, 03/08/20-07/08/20, ACM : Association for Computing Machinery, (en ligne), août 2020.
Résumé Accès : https://arxiv.org/abs/2003.02869 – https://doi.org/10.1145/3382734.3405752 – https://oatao.univ-toulouse.fr/26404/
BibTeXAdam Shimi, Aurélie Hurault, Philippe Quéinnec
Derivation of Heard-Of Predicates From Elementary Behavioral Patterns (regular paper)
Dans : International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2020), Online, 15/06/20-19/06/20, juin 2020.
Accès : https://arxiv.org/abs/2004.10619 – https://oatao.univ-toulouse.fr/26385/
BibTeXXavier Thirioux, Alexis Maffart
Taylor Series Revisited (regular paper)
Dans : International Colloquium on Theoretical Aspects of Computing (ICTAC 2019), Hammamet, Tunisia, 31/10/19-04/11/19, Vol. 11884, Springer, Lecture Notes in Computer Science, p. 335-352, novembre 2019.
Résumé Accès : https://doi.org/10.1007/978-3-030-32505-3_19 – https://oatao.univ-toulouse.fr/26358/
BibTeXUlrich Berger, Ralph Matthes, Anton Setzer
Martin Hofmann’s case for non-strictly positive data types (regular paper)
Dans : International Conference on Types for Proofs and Programs (TYPES 2018), Braga, Portugal, 18/06/18-21/06/18, Vol. 130, Peter Dybjer, José Espírito Santo, Luís Pinto (Eds.), Schloss Dagstuhl Leibniz-Zentrum fur Informatik, LIPIcs : Leibniz International Proceedings in Informatics, p. 1-22, novembre 2019.
Résumé Accès : https://doi.org/10.4230/LIPIcs.TYPES.2018.1
BibTeXDominique Larchey-Wendling, Ralph Matthes
Certification of Breadth-First Algorithms by Extraction (regular paper)
Dans : International Conference on Mathematics of Program Construction (MPC 2019), Porto, 07/10/19-09/10/19, Vol. 11825, Graham Hutton (Eds.), Springer Nature Switzerland, LNCS, p. 45-75, octobre 2019.
Résumé Accès : https://doi.org/10.1007/978-3-030-33636-3_3
BibTeXArmando Castañeda, Aurélie Hurault, Philippe Quéinnec, Matthieu Roy
Tasks in Modular Proofs of Concurrent Algorithms (regular paper)
Dans : International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2019), Pisa, Italia, 22/10/19-25/10/19, Springer, Lecture Notes in Computer Science 11914, p. 69-83, octobre 2019.
Résumé Accès : http://arxiv.org/abs/1909.05537 – https://doi.org/10.1007/978-3-030-34992-9_6 – https://oatao.univ-toulouse.fr/26273/
BibTeXJean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (regular paper)
Dans : Formal Methods (FM 2019), Porto, 07/10/19-11/10/19, Vol. 11800, Maurice N. ter Beek, Annabelle McIver, José N. Oliveira (Eds.), Springer, Lecture Notes in Computer Science, p. 45-63, octobre 2019.
Accès : https://hal.archives-ouvertes.fr/hal-02332531/
BibTeXFlorent Chevrou, Aurélie Hurault, Shin Nakajima, Philippe Quéinnec
A Map of Asynchronous Communication Models (regular paper)
Dans : Refinement Workshop, in World Congress on Formal Methods (REFINE 2019), Porto, Portugal, 07/10/19-07/10/19, octobre 2019.
Aurélie Hurault, Philippe Quéinnec
Proving a Non-Blocking Algorithm for Process Renaming with TLA+ (regular paper)
Dans : Tests and Proofs (TAP 2019), Porto, Portugal, 09/10/19-11/10/19, Vol. 11823, Springer, Lecture Notes in Computer Science, p. 147-166, octobre 2019.
Accès : https://oatao.univ-toulouse.fr/24978/1/hurault_24978.pdf – https://doi.org/10.1007/978-3-030-31157-5_10 – https://oatao.univ-toulouse.fr/24978/
BibTeXSara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec
A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations (regular paper)
Dans : International Conference on Business Process Management (BPM 2019), Vienna, Austria, 01/09/19-06/09/19, Vol. 11675, Springer, Lecture Notes in Computer Science, p. 52-68, septembre 2019 (Best Paper Award).
Accès : https://doi.org/10.1007/978-3-030-26619-6_6 – https://oatao.univ-toulouse.fr/24922/
BibTeX
Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Dans : Journées du Groupe de Travail Vérification du GDR GPL, Nantes, 17/06/19-19/06/19 (conférencier invité).
Erik Martin-Dorel, Sergei Soloviev
Cumulative Effects in Learning
Dans : Conference on Artificial Intelligence and Theorem Proving (AITP), Aussois, France, 25/03/18-30/03/18.
Accès : http://aitp-conference.org/2018/aitp18-proceedings.pdf
BibTeXErik Martin-Dorel, Pierre Roux
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
Dans : Journées FAC 2017, Onera, Toulouse, 29/03/17-30/03/17.
Accès : http://projects.laas.fr/IFSE/FAC/previous/journées-fac-2017/
BibTeXStéphane Le Roux, Erik Martin-Dorel, Jan-Georg Smaus
Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle
Dans : Journées FAC 2017, Onera, Toulouse, 29/03/17-30/03/17.
Accès : http://projects.laas.fr/IFSE/FAC/previous/journ%C3%A9es-fac-2017/
BibTeXBadr Siala, Tahar Bhiri, Jean-Paul Bodeveix, Mamoun Filali
An Event-B development process for the distributed BIP framework
Dans : FAC, Toulouse, 30/03/16-31/03/16.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
Dans : Journées FAC 2016, LAAS, Toulouse, 30/03/16-31/03/16.
Accès : http://projects.laas.fr/IFSE/FAC/previous/journ%C3%A9es-fac-2016/
BibTeXErik Martin-Dorel, Guillaume Melquiond
CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq
Dans : The MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, CIRM, Luminy, Marseille, 11/01/16-15/01/16.
Accès : http://scientific-events.weebly.com/1508.html
BibTeXFormal proofs and certified computation in Coq
Dans : The French Symposium on Games – Theory and Applications, Université Paris Diderot, 26/05/15-30/05/15.
Ning Ge, Marc Pantel, Xavier Crégut
Probabilistic Failure Analysis in Model Validation & Verification
Dans : Formalisation des Activités Concurrentes, Toulouse, 16/04/14-17/04/14.
Evgeny Dantsin, Jan-Georg Smaus, Sergei Soloviev
Algorithms in Games Evolving in Time: Winning Strategies Based on Testing Hypotheses
Dans : Isabelle Users Workshop of the International Conference on Interactive Theorem Proving, Princeton, USA, 12/08/12-12/08/12, Tobias Nipkow, Larry Paulson, Makarius Wenzel (Eds.).
Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Roberto Sangiovanni-Vincentelli, Werner Damm, Thomas Henzinger, Kim Larsen
Contracts for System Design, Now Publishers, 2018.
Accès : https://www.nowpublishers.com/article/Details/EDA-053
BibTeXAbdeldjalil Boudjadar, Jean-Paul Bodeveix, Mamoun Filali
Revising and Extending the Uppaal Communication Mechanism, Springer-Verlag, Vol. 7306, Lecture Notes in Computer Science, juin 2012.
Olga Antonova, Sergei Soloviev
La théorie et la pratique de la réalité virtuelle: l’analyse logique et philosophique., Universite d’Etat de St. Petersbourg, août 2008.
J.-M. Farines, Bernard Berthomieu, Jean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, Hicham Hafidi, Jean-Luc Lambert, Pierre Michel, François Vernadat
The Cotre Project: Rigorous Software Development for Real Time Systems in Avionics, COLNARIC, ADAMSKI & WEGRZYN, novembre 2003.
Jean-Paul Bodeveix, Mamoun Filali, Amal Sayah
Programmation en C++, InterEditions, 1994.
Yamine Ait Ameur, Shin Nakajima, Dominique Méry
Implicit and explicit semantics integration in proof based developments of discrete systems
, Springer, 2020 (à paraître).
Accès : http://shonan.nii.ac.jp/shonan/blog/2015/11/10/implicit-and-explicit-semantics-integration-in-proof-based-developments-of-discrete-systems/
BibTeXPierre Dissaux, Mamoun Filali, Pierre Michel, François Vernadat
Architecture Description languages
, Springer, avril 2005.
Jean-Paul Bodeveix, Thierry Millan, Christian Percebois, Pierre Bazex, Louis Féraud
NEPTUNE : Method, Checking and documentation generation for UML application
, NEPTUNE Consortium, 2003.
Guillaume Babin, Yamine Ait Ameur, Marc Pantel
A generic model for system substitution
Dans : Trustworthy Cyber-Physical Systems Engineering. Alexander Romanovsky, Fuyuki Ishikawa (Eds.) , Chapman & Hall, CRC Press, 4, p. 75-103, Computer and Information Science Series, septembre 2016.
Accès : https://www.crcpress.com/Trustworthy-Cyber-Physical-Systems-Engineering/Romanovsky-Ishikawa/9781498742450
BibTeXTimothy Wang, Romain Jobredeaux, Heber Henrencia, Pierre-Loïc Garoche, Eric Feron, Marc Pantel
From Design to Implementation: An Automated Credible Autocoding Chain for Control Systems
Dans : Advances in Control System Technology for Aerospace Applications. Eric Féron (Eds.) , Springer-Verlag, p. 137-180, 2016.
Explicitation de la sémantique du domaine dans les modèles de systèmes/ Une approche à base d’ontologies.
Thèse de doctorat, Institut National Polytechnique de Toulouse, mars 2018.
Formalisations pour les compositions de services
Habilitation à diriger des recherches, Institut National Polytechnique de Toulouse, juillet 2018.
Modular Avionics Software Integration on Multi-Core COTS : certification-Compliant Methodology and Timing Analysis Metrics for Legacy Software Reuse in Modern Aerospace Systems
Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2017.
A formal approach for correct-by-construction system substitution
Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2017.
Formalisation of Asynchronous Interactions
Thèse de doctorat, Institut National Polytechnique de Toulouse, novembre 2017.
Décomposition formelle des spécifications centraliseées Event-B : application aux systèmes distribués BIP
Thèse de doctorat, Université Paul Sabatier, décembre 2017.
Verifying Embedded Systems
Habilitation à diriger des recherches, Institut National Polytechnique de Toulouse, septembre 2016.
Systematic use of models of concurrency in executable domain-specific modelling languages
Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2016.
Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes
Thèse de doctorat, Université de Toulouse, mars 2016.
Une théorie mécanisée des arbres réguliers en théorie des types dépendants
Thèse de doctorat, Université Paul Sabatier, mai 2016.
Erik Martin-Dorel, Sergei Soloviev
A Formal Study of Boolean Games with Random Formulas as Pay Functions
Rapport de recherche, IRIT/RR–2017–01–FR, IRIT, février 2017.
Accès : https://www.irit.fr/publis/ACADIE/IRIT-RR-2017-01-FR.pdf
BibTeXJavier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker
Rapport de recherche, 0, Archive of Formal Proofs, septembre 2016.
Accès : https://www.isa-afp.org/entries/CAVA_LTL_Modelchecker.shtml
BibTeXZhibin Yang, Jean-Paul Bodeveix, Mamoun Filali
Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties
Rapport de recherche, IRIT/RT–2014-02–FR, IRIT, décembre 2014.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions in Coq
Rapport de recherche, IRIT/RR–2014-09–FR, IRIT, novembre 2014.
Accès : http://www.irit.fr/publis/ACADIE/IRIT-RR-2014-09-FR.pdf
BibTeXManuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Concurrent Systems with Priorities
Rapport de recherche, Report–2013-16–FR, IRIT, juin 2013.
Résumé Accès : http://www.irit.fr/~Manuel.Garnacho/Publications/MechPrio.pdf
BibTeXManuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Concurrent Systems with Priorities
Rapport de recherche, RIT/RR–2013-16–FR, IRIT, février 2013.
Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Real-Time Concurrent Systems
Rapport de recherche, IRIT/RR–2013-15–FR, IRIT, janvier 2013.
Univariate and Bivariate Integral Roots Certificates Based on Hensel’s Lifting
Rapport de recherche, RRLIP2011-1, LIP, Ecole Normale Supérieure de Lyon, mars 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Verification of Timed BPEL 2.0 Models
Rapport de recherche, IRIT/RR2011-10FR, IRIT, mars 2011.
Jacques Cazin, Pierre-Loïc Garoche, Marc Pantel, Virginie Wiels
D2.5.1 ES_PASS qualification guidelines for static analysis based verification tools
Rapport de contrat, D2.5.1, Institut National Polytechnique de Toulouse, novembre 2009.
contrats de l’équipe
| Acronyme | Titre | Resp. sc | Début – fin | |
|---|---|---|---|---|
| FORMEDICIS |  | Méthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques | Yamine AIT AMEUR | 2016 – 2021 |
| PARDI | | Vérification de systèmes distribués paramétrés | Philippe QUéINNEC | 2016 – 2021 |
| DISCONT | | Intégration correcte de modèles discrets et continus | Neeraj SINGH | 2017 – 2022 |
| IMPEX [Contrat terminé] | Integration des semantique implicite et explicite dans le développement de systèmes discrets fondés sur la panne | Yamine AIT AMEUR | 2013 – 2017 | |
| VORACE [Contrat terminé] | | Vérification des optimisations rapides appliquées à la commande embarquée | Marc PANTEL | 2013 – 2016 |
| CLIMT [Contrat terminé] |  | Méthodes catégoriques et logiques en transformations de modèles | Ralph MATTHES | 2012 – 2016 |
| GeMoC [Contrat terminé] | GeMoC : Un framework de modèles de calcul génériques pour l’éxecution et l’analyse dynamique de modèles | Xavier CRéGUT | 2012 – 2016 | |
| Verisync [Contrat terminé] | | Vérification formelle d’un générateur de code pour un langage synchrone | Martin STRECKER | 2010 – 2014 |
| ITEmIS [Contrat terminé] | Systèmes d’information et embarqués intégrés | Mamoun FILALI | 2008 – 2011 |
| Acronyme | Titre | Resp. sc | Début – fin | |
|---|---|---|---|---|
| OPEES [Contrat terminé] | | Plateforme ouverte pour ingénierie des systèmes embarqués | Marc PANTEL | 2009 – 2012 |
| Acronyme | Titre | Resp. sc | Début – fin | |
|---|---|---|---|---|
| INP2011-003 [Contrat terminé] | Modélisation des dépendances entre fonctions de niveau avion pour l’analyse des risques | Yamine AIT AMEUR | 2011 – 2012 | |
| TOPCASED [Contrat terminé] | TOPCASED – Toolkit in open source for Critical Application & SystEms Development | Mamoun FILALI Christian PERCEBOIS | 2006 – 2010 |