Equipe ACADIE

Responsable :

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

Méthodes formelles
Vérification & validation
Environnements de preuve
Systèmes critiques
Modélisation

personnel de l’équipe

Membres permanents
    Membres non – permanents
      Membres rattachés

        publications de l’équipe

        Articles dans des revues internationales
      • Adam Shimi, Aurélie Hurault, Philippe Quéinnec

        Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models

        Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, 17 (3), pp.26:1 – 26:43. ⟨10.46298/lmcs-17(3:26)2021⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03352272

      • Guillaume Dupont, Yamine Ait-Ameur, Neeraj Kumar Singh, Marc Pantel

        Event-B Hybridation: A Proof and Refinement-based Framework for Modelling Hybrid Systems

        ACM Transactions on Embedded Computing Systems (TECS), ACM, 2021, 20 (4, Article 35), pp.1-37. ⟨10.1145/3448270⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03266069

      • Neeraj Kumar Singh, Yamine Aït-Ameur, Romain Geniet, Dominique Méry, Philippe Palanque

        On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications

        Interacting with Computers, Oxford University Press (OUP), 2021, ⟨10.1093/iwcomp/iwab016⟩

        Accès: https://hal.inria.fr/hal-03224780

      • José Espírito Santo, Ralph Matthes, Luís Pinto

        A Coinductive Approach to Proof Search through Typed Lambda-Calculi

        Annals of Pure and Applied Logic, Elsevier Masson, 2021, 172 (10), ⟨10.1016/j.apal.2021.103026⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03086504

      • Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec, Laïd Kahloud

        A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations

        Information Systems, Elsevier, In press

        Accès: https://hal.archives-ouvertes.fr/hal-03170863

      • Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali

        Event-B formalization of a variability-aware component model patterns framework

        Science of Computer Programming, Elsevier, 2020, 199, ⟨10.1016/j.scico.2020.102511⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03097697

      • Maxim Kolomeets, Amira Benachour, Didier El Baz, Andrey Chechulin, Martin Strecker, Igor Kotenko

        Reference architecture for social networks graph analysis tool

        Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, Innovative Information Science & Technology Research Group (ISYOU), 2019, 10 (4), pp.109-125. ⟨10.22667/JOWUA.2019.12.31.109⟩

        Accès: https://hal.laas.fr/hal-02443865

      • Florent Chevrou, Aurélie Hurault, Philippe Quéinnec

        A Modular Framework for Verifying Versatile Distributed Systems

        Journal of Logic and Algebraic Methods in Programming, Elsevier, 2019, 108, pp.24-46. ⟨10.1016/j.jlamp.2019.05.008⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02451058

      • Fei Wang, Zhibin Yang, Zhi-Qiu Huang, Cheng-Wei Liu, Yong Zhou, Jean-Paul Bodeveix, M Filali

        An Approach to Generate the Traceability Between Restricted Natural Language Requirements and AADL Models

        IEEE Transactions on Reliability, Institute of Electrical and Electronics Engineers, 2019, 1 (1), pp.1-20. ⟨10.1109/TR.2019.2936072⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02382714

      • José Espírito Santo, Ralph Matthes, Luís Pinto

        Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search

        Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2019, 29 (8), pp.1092-1124. ⟨10.1017/S0960129518000099⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02360678

      • 503 Service Temporarily Unavailable

        Service Temporarily Unavailable

        The server is currently unable to handle the request due to a temporary overloading or maintenance of the server.

        503 Service Temporarily Unavailable

        Service Temporarily Unavailable

        The server is currently unable to handle the request due to a temporary overloading or maintenance of the server.

        Conférences et workshops internationaux avec actes édités et comité de lecture
      • Ismail Mendil, Yamine Aït-Ameur, Neeraj K. Singh, Dominique Méry, Philippe Palanque

        Standard Conformance-by-Construction with Event-B

        26th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2021), European Research Consortium for Informatics and Mathematics: ERCIM, Working Group on Formal Methods for Industrial Critical Systems, Aug 2021, Paris (virtual), France. pp.126-146, ⟨10.1007/978-3-030-85248-1_8⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03328649

      • Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil

        Sound Verification Procedures for Temporal Properties of Infinite-State Systems

        33rd International Conference on Computer-Aided Verification (CAV 2021), Jul 2021, Los Angeles (Online), United States

        Accès: https://hal.archives-ouvertes.fr/hal-03243129v2

      • Erwan Le Merrer, Benoît Morgan, Gilles Trédan

        Setting the Record Straighter on Shadow Banning

        INFOCOM 2021 – IEEE International Conference on Computer Communications, IEEE, May 2021, Virtual, Canada. pp.1-10, ⟨10.1109/INFOCOM42981.2021.9488792⟩

        Accès: https://hal.inria.fr/hal-03234771

      • Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec

        A Direct Formal Semantics for BPMN Time-Related Constructs

        16th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2021), Apr 2021, online, Czech Republic. ⟨10.5220/0010462901380149⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03170814

      • Guillaume Dupont, Yamine Aït-Ameur, Neeraj Singh, Fuyuki Ishikawa, Tsutomu Kobayashi, Marc Pantel

        Embedding Approximation in Event-B: Safe Hybrid System Design Using Proof and Refinement

        22nd International Conference on Formal Engineering Methods (ICFEM 2020), Mar 2021, Singapour, Singapore. pp.251-267, ⟨10.1007/978-3-030-63406-3_15⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03266056

      • Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, Neeraj Kumar Singh

        An Event-B Based Generic Framework for Hybrid Systems Formal Modelling

        16th International Conference on Integrated Formal Methods (IFM 2020), Nov 2020, Lugano (virtual), Switzerland. pp.82-102, ⟨10.1007/978-3-030-63461-2_5⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03265788

      • Nikolena Christofi, Claude Baron, X Pucel, Marc Pantel, M Machin, C Ducamp

        Adopting a model-based approach for satellite operations’ diagnosis

        13ème Conférence Internationale de Modélisation, Optimisation et Simulation (MOSIM 2020), Nov 2020, Agadir, Morocco

        Accès: https://hal.laas.fr/hal-02946817

      • Erwan Le Merrer, Benoît Morgan, Gilles Trédan

        Bug ou ban ? Une Perspective Topologique sur le Shadow Banning

        ALGOTEL 2020 – 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Sep 2020, Lyon, France. pp.1-4

        Accès: https://hal.archives-ouvertes.fr/hal-02875595

      • Jean-Baptiste Raclet, Franck Silvestre

        Git4School: A Dashboard for Supporting Teacher Interventions in Software Engineering Courses

        EC-TEL 2020 – Fifteenth European Conference on Technology Enhanced Learning, Sep 2020, Heidelberg (GER) Online, France. pp.392-397, ⟨10.1007/978-3-030-57717-9_33⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02946555

      • Adam Shimi, Armando Castañeda

        K-set agreement bounds in round-based models through combinatorial topology

        39th ACM Symposium on Principles of Distributed Computing (PODC 2020), Aug 2020, Salerno, Italy. pp.395-404

        Accès: https://hal.archives-ouvertes.fr/hal-02950742

      • Conférences et workshops nationaux avec actes édités et comité de lecture
      • Hélène Fargier, Érik Martin-Dorel, Pierre Pomeret-Coquot

        Jeux incomplets algébriques

        Rencontres des Jeunes Chercheurs en Intelligence Artificielle (RJCIA 2021) @ Plate-Forme Intelligence Artificielle (PFIA 2021), Jul 2021, Bordeaux, France. pp.46-53

        Accès: https://hal.archives-ouvertes.fr/hal-03298722

      • Aurélie Hurault, Philippe Quéinnec

        Proving a Non-Blocking Algorithm for Process Renaming with TLA+

        13th International Conference on Tests and Proofs (TAP 2019), part of the 3rd World Congress on Formal Methods, Oct 2019, Porto, Portugal. pp.147-166

        Accès: https://hal.archives-ouvertes.fr/hal-02442015

      • Florent Chevrou, Aurélie Hurault, Shin Nakajima, Philippe Quéinnec

        A Map of Asynchronous Communication Models

        Refinement Workshop, in World Congress on Formal Methods (REFINE 2019), Oct 2019, Porto, Portugal. pp.1-15, ⟨10.1007/978-3-030-54997-8_20⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02930097

      • 503 Service Temporarily Unavailable

        Service Temporarily Unavailable

        The server is currently unable to handle the request due to a temporary overloading or maintenance of the server.

        Livres (monographies)
      • José Espírito Santo, Ralph Matthes, Luís Pinto

        Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic

        Ugo de’Liguoro; Stefano Berardi; Thorsten Altenkirch. LIPIcs : 26th International Conference on Types for Proofs and Programs (TYPES 2020), 188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany, 2021, LIPIcs : Leibniz International Proceedings in Informatics ; ISSN : 1868-8969, 978-3-95977-182-5. ⟨10.4230/LIPIcs.TYPES.2020.4⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03255968

      • Yamine Aït-Ameur, Régine Laleau, Dominique Méry, Neeraj Kumar Singh

        Towards Leveraging Domain Knowledge in State-Based Formal Methods

        Raschke, Alexander; Riccobene, Elvinia; Schewe, Klaus-Dieter. Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Brger on the Occasion of His 75th Birthday”, Lecture Notes in Computer Science (12750), Springer, pp.1-13, 2021, Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Brger on the Occasion of His 75th Birthday, 978-3-030-76020-5. ⟨10.1007/978-3-030-76020-5_1⟩

        Accès: https://hal.inria.fr/hal-03250787

      • Yamine Aït-Ameur, Shin Nakajima, Dominique Méry

        Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems

        Springer Singapore, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6⟩

        Accès: https://hal.inria.fr/hal-02910199

      • Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry

        Formal Ontological Analysis for Medical Protocols

        Implicit and explicit semantics integration in proof based developments of discrete systems, Springer, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6_5⟩

        Accès: https://hal.inria.fr/hal-03199742

      • Ulrich Berger, Ralph Matthes, Anton Setzer

        Martin Hofmann’s Case for Non-Strictly Positive Data Types

        Peter Dybjer; José Espírito Santo; Luís Pinto. 24th International Conference on Types for Proofs and Programs (TYPES 2018), 130, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp.1:1-1:22, 2019, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-106-1. ⟨10.4230/LIPIcs.TYPES.2018.1⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02365814

      • Benedikt Ahrens, Ralph Matthes

        Heterogeneous Substitution Systems Revisited

        Tarmo Uustalu. 21st International Conference on Types for Proofs and Programs (TYPES 2015), 69, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp.2:1-2:23, 2018, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-030-9. ⟨10.4230/LIPIcs.TYPES.2015.2⟩

        Accès: https://hal.archives-ouvertes.fr/hal-02360681

      • Ladjel Bellatreche, Yamine Aït-Ameur, George Angelos Papadopoulos

        Models and Data Engineering

        Ladjel Bellatreche; Yamine Ait Ameur; George Angelos Papadopoulos. Future Generation Computer Systems, 68, Elsevier, 2017, Models and data engineering, ⟨10.1016/j.future.2016.11.017⟩

        Accès: https://hal.archives-ouvertes.fr/hal-03128351

      • 503 Service Temporarily Unavailable

        Service Temporarily Unavailable

        The server is currently unable to handle the request due to a temporary overloading or maintenance of the server.

        Thèses et habilitations
      • Adam Shimi

        On the Power of Rounds: Explorations of the Heard-Of Model

        Distributed, Parallel, and Cluster Computing [cs.DC]. Université de Toulouse, 2020. English

        Accès: https://hal.archives-ouvertes.fr/tel-03123969

      • Ian Malakhovski

        Sur le pouvoir expressif des structures applicatives et monadiques indexées

        Analyse numérique [cs.NA]. Université Paul Sabatier – Toulouse III, 2019. Français. ⟨NNT : 2019TOU30118⟩

        Accès: https://tel.archives-ouvertes.fr/tel-02735749

      • Aurélie Hurault

        Formalisations pour les compositions de services

        Informatique [cs]. Institut National Polytechnique de Toulouse (Toulouse INP), 2018

        Accès: https://hal-univ-tlse3.archives-ouvertes.fr/tel-03282922

      • 503 Service Temporarily Unavailable

        Service Temporarily Unavailable

        The server is currently unable to handle the request due to a temporary overloading or maintenance of the server.

        Rapports
      • Albert Benveniste, Kim Larsen, Jean-Baptiste Raclet

        Mixed Nondeterministic-Probabilistic Interfaces

        [Research Report] RR-9372, Inria Rennes Bretagne Atlantique; Aalborg University; Université de Toulouse 3 Paul Sabatier. 2020, pp.40

        Accès: https://hal.inria.fr/hal-02985273

      • Érik Martin-Dorel, Sergei Soloviev

        A Formal Study of Boolean Games with Random Formulas as Pay Functions

        [Research Report] IRIT. 2017

        Accès: https://hal.archives-ouvertes.fr/hal-03109258

      • 503 Service Temporarily Unavailable

        Service Temporarily Unavailable

        The server is currently unable to handle the request due to a temporary overloading or maintenance of the server.

        contrats de l’équipe

        AcronymeTitreResp. scDébut – fin
        AcronymeTitreResp. scDébut – fin
        AcronymeTitreResp. scDébut – fin
        Jeudi 14 Janvier 2021, 15h00
        Conception Correcte par Construction de Systèmes Hybrides Basée sur le Raffinement et la Preuve
        Guillaume DUPONT – Equipe ACADIE, IRIT INP-ENSEEIHT, En visioconférence
        #these
        Lundi 14 Septembre 2020, 10h00
        Un environnement formel pour la sémantique des systèmes hétérogènes
        Mathieu MONTIN – Equipe ACADIE, IRIT INP-ENSEEIHT, Auditorium et via visioconférence
        #these
        Vendredi 12 Juin 2020, 14h00
        Transformations sémantiques pour l’évolution des modèles de données
        Lynda AIT OUBELLI – Equipe ACADIE, IRIT INP-ENSEEIHT, En visioconférence
        #these
        Mardi 15 Octobre 2019, 14h00
        Sur le pouvoir expressif des structures applicatives et monadiques indexées
        Ian MALAKHOVSKI – Equipe ACADIE, IRIT UT3 Paul Sabatier, IRIT, Salle 001
        #these
        Vendredi 15 Décembre 2017, 9h00
        Formal decomposition of Event-B centralized specifications: application to BIP distributed systems
        Badr SIALA – Equipe ACADIE – IRIT UT3 Paul Sabatier, IRIT, Salle des Thèses
        #these
        Mercredi 22 Novembre 2017, 10h15
        Formalisation des interactions asynchrones
        Florent CHEVROU – Equipe ACADIE – IRIT INP-ENSEEIHT, Salle des thèses
        #these
        Jeudi 6 Juillet 2017, 9h30
        A formal approach for correct-by-construction system substitution
        Guillaume BABIN – Equipe ACADIE – IRIT ENSEEIHT, Amphi A001
        #these
        Mercredi 5 Juillet 2017, 9h30
        Modular avionics software integration on multicore COTS: certification-compliant methodology and timing analysis metrics for legacy software reuse…
        Soukayna M’SIRDI – Equipe ACADIE – IRIT ENSEEIHT, Amphi A001
        #these
        Mercredi 13 Juillet 2016, 11h00
        Systematic Use of Models of Concurrency in eXecutable Domain-Specific Modeling Languages
        Florent LATOMBE – Equipe ACADIE – IRIT Salle du Conseil, F501
        #these
        Jeudi 19 Mai 2016, 10h00
        Une théorie mécanisée des arbres réguliers en théorie des types dépendants
        Régis SPADOTTI – Equipe ACADIE – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
        #these
        Lundi 28 Octobre 2019 – Jeudi 31 Octobre 2019
        MEDI 2019 : 9th International Conference on Model and Data Engineering
        INP-ENSEEIHT
        #congres En savoir plus
        Lundi 26 Juin 2017 – Vendredi 30 Juin 2017
        École Jeunes Chercheurs en Programmation 2017 (EJCP 2017)
        INP-ENSEEIHT, Toulouse
        #congres En savoir plus
        Lundi 12 Décembre 2016 – Vendredi 16 Décembre 2016
        World Champions Programming School at Toulouse
        UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
        #congres En savoir plus
        Mercredi 18 Juin 2014 – Vendredi 20 Juin 2014
        LACL 2014 : Logical Aspects of Computational Linguistics
        UT3 Paul Sabatier, IRIT
        #congres En savoir plus
        Lundi 2 Juin 2014 – Jeudi 5 Juin 2014
        ABZ 2014 : 4th International Conference ASM, Alloy, B, TLA, VDM, Z
        Toulouse
        #congres En savoir plus
        Jeudi 27 Février 2020, 16h00 – 17h00
        Défis de génie logiciel dans l’évolution collaborative de l’assistant de preuve Coq et son écosystème
        Théo ZIMMERMANN – Inria, Université de Paris, IRIF, CNRS UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
        #seminaire
        Jeudi 26 Septembre 2019, 14h00 – 15h00
        Security and Privacy in Smart Environments
        Andrey CHECHULIN – Saint-Petersbourg Institute for Informatics and Automatisation (Russie) UT3 Paul Sabatier, IRIT, Salle 003
        #seminaire
        Mercredi 29 Mai 2019, 14h30 – 15h30
        Sécurité avec SGAC et ASTD
        Marc FRAPPIER – Université de Sherbrooke, Groupe de recherche en informatique fondamentale (GRIF) (Canada) INP-ENSEEIHT, Salle des thèses
        #seminaire
        Vendredi 16 Février 2018, 10h30 – 12h00
        Algorithmes naturels et systèmes d’influence
        Bernadette CHARRON-BOST – Laboratoire d’informatique de l’École Polytechnique (LIX) (France) INP-ENSEEIHT, Salle des thèses
        #seminaire
        Mardi 21 Février 2017, 16h00 – 17h30
        Symbolic Dynamics, Asymptotic Combinatorics and Game Theory
        Nicolaï VASILYEV – Inst. de Mathématiques Steklov, St. Petersbourg (Russie) UT3 Paul Sabatier, IRIT, Salle 001
        #seminaire
        Mardi 10 Janvier 2017, 14h00 – 15h30
        A new dimension of Cloud Governance
        Ernesto PIMENTEL – Université de Malaga (Espagne) INP-ENSEEIHT, Salle des thèses
        #seminaire
        Lundi 12 Décembre 2016, 14h00 – 15h30
        Challenges in Certification of Model-Based Design of Cyber-Physical Systems
        Alain WASSYNG – Université de Mac Master, Hamilton, Ontario (Canada) ENSEEIHT, Amphitheâtre A001
        #seminaire
        Mardi 2 Septembre 2014, 11h00
        Verified Decision Procedures for Regular Expression Equivalence
        Tobias NIPKOW – Technische Universität München (Allemagne) UT3 Paul Sabatier, IRIT, Salle des Thèses
        #seminaire
        Jeudi 23 Janvier 2014, 14h00
        From MTL to deterimistic timed automata
        Dejan NICKOVIC – Austrian Institute of Technology (Autriche) UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
        #seminaire
        Vendredi 6 Juillet 2018, 9h30
        Formalisations pour les compositions de services
        Aurélie HURAULT – Equipe ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
        #hdr
        Lundi 19 Septembre 2016, 9h30
        Verifying Embedded Systems
        Xavier THIRIOUX – Equipe ACADIE – IRIT INP-ENSEEIHT, Salle des theses
        #hdr
        Jeudi 25 Juin 2015
        Journée du GDR GPL – Génie Logiciel et Transfert Technologique
        UT3 Paul Sabatier, IRIT
        #journee
        Mercredi 22 Avril 2015 – Jeudi 23 Avril 2015
        Journées FAC’2015 : Formalisation des Activités Concurrentes
        INP-ENSEEIHT, Salle des theses
        #journee