Head : Jan-Georg SMAUS

ACADIE (Assistance à la Certification d’Applications DIstribuées et Embarquées) team is concerned with the formal and mechanized verification of systems.

Formalisation is required to assert rigorous properties on the systems, and mechanization is used to guarantee the validity of the verification.

Acadie is agnostic with regard to the used formalisms as long as they are theoretically well-founded and tool-assisted. Application domains have considered cyber-physical systems, embedded and real-time systems, distributed systems, interactive systems…


Formal methods
Verification and validation
Proof environments
Critical systems

Members team

Permanent members
Non-permanent members
External members

publications team

International journals articles
  • Armando Castañeda, Aurélie Hurault, Philippe Quéinnec, Matthieu Roy

    Tasks in modular proofs of concurrent algorithms

    Information and Computation, 2023, 292 (Selected papers from SSS’2019, the 21st International Symposium on Stabilization, Safety, and Security of Distributed Systems), pp.105040. ⟨10.1016/j.ic.2023.105040⟩


  • Nikolena Christofi, Xavier Pucel, Claude Baron, Marc Pantel, Sebastien Guilmeau, Christophe Ducamp

    Toward an Operations-Dedicated Model for Space Systems

    Journal of Aerospace Information Systems, 2023, pp.1-13. ⟨10.2514/1.I011093⟩


  • Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Guillaume Dupont, Dominique Méry, Philippe Palanque

    Formal domain-driven system development in Event-B: Application to interactive critical systems

    Journal of Systems Architecture, 2023, 135, pp.102798. ⟨10.1016/j.sysarc.2022.102798⟩


  • Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel

    Games of Incomplete Information: a Framework Based on Belief Functions

    International Journal of Approximate Reasoning, 2022, 151, pp.182-204. ⟨10.1016/j.ijar.2022.09.010⟩


  • Peter Riviere, Neeraj Kumar Singh, Yamine Aït-Ameur

    Reflexive Event-B: Semantics and Correctness The EB4EB framework

    IEEE Transactions on Reliability, 2022, pp.1-16. ⟨10.1109/TR.2022.3219649⟩


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

    Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B

    Science of Computer Programming, 2022, 216, pp.102765. ⟨10.1016/j.scico.2021.102765⟩


  • 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, 2022, 104, pp.101765. ⟨10.1016/⟩


  • Neeraj Kumar Singh, Yamine Aït-Ameur, Ismail Mendil, Dominique Méry, David Navarre, Philippe Palanque, Marc Pantel

    F3FLUID: A formal framework for developing safety‐critical interactive systems in FLUID

    Journal of Software: Evolution and Process, In press, ⟨10.1002/smr.2439⟩


  • 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, 2021, 17 (3), pp.26:1 – 26:43. ⟨10.46298/lmcs-17(3:26)2021⟩


  • Zhibin Yang, Zhikai Qiu, Yong Zhou, Zhiqiu Huang, Jean-Paul Bodeveix, M Filali

    C2AADL_Reverse: A model-driven reverse engineering approach to development and verification of safety-critical software

    Journal of Systems Architecture, 2021, 118, pp.102202. ⟨10.1016/j.sysarc.2021.102202⟩


  • National journals articles
  • Jean-Baptiste Raclet, Franck Silvestre, Mika Pons

    Git4School : un tableau de bord pour assister la prise de décisions de l’enseignant lors des cours de génie logiciel

    STICEF (Sciences et Technologies de l’Information et de la Communication pour l’Éducation et la Formation), 2021, Numéro Spécial : Technologies pour l’apprentissage de l’Informatique de la maternelle à l’université, 28 (3), pp.1-20. ⟨10.23709/sticef.28.3.2⟩


  • National journals articles
    Special issues of journal
    International conferences articles
  • Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann

    Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users

    14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Białystok, Poland. pp.1-18


  • Peter Riviere, Neeraj Singh, Yamine Aït-Ameur, Guillaume Dupont

    Standalone Event-B models analysis relying on the EB4EB meta-theory

    9th International Conference on Rigorous State-based Methods (ABZ 2023), LORIA : laboratoire lorrain de recherche en informatique et ses applications, Université de Lorraine, May 2023, Nancy, France


  • Peter Riviere, Neeraj Kumar Singh, Yamine Aït-Ameur, Guillaume Dupont

    Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework

    NASA Formal Methods (NFM 2023), NASA: National Aeronautics and Space Administration, May 2023, Houston, United States. pp.1-18


  • Hélène Fargier, Érik Martin-Dorel, Pierre Pomeret-Coquot

    Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant

    Ecole Jeunes Chercheuses et Chercheurs en Informatique Mathématique, Maison de la Modélisation, de la Simulation et des Interactions [MSI], Jun 2022, Nice, France


  • Nikolena Christofi, Xavier Pucel, Claude Baron, Marc Pantel, Sébastien Guilmeau, Christophe Ducamp

    Towards an agile, model-based multidisciplinary process to improve operational diagnosis in complex systems

    11th European Congress on Embedded real time systems (ERTS 2022),, Jun 2022, Toulouse, France


  • Peter Riviere, Neeraj Kumar Singh, Yamine Aït-Ameur

    EB4EB: A Framework for Reflexive Event-B

    26th International Conference on Engineering of Complex Computer Systems (ICECCS 2022), Mar 2022, Hiroshima, Japan. pp.71-80, ⟨10.1109/ICECCS54210.2022.00017⟩


  • Md Siddiqur Rahman, Laurent Lapasset, Josiane Mothe

    Multi-label Classification of Aircraft Heading Changes using Neural Network to Resolve Conflicts

    14th International Conference on Agents and Artificial Intelligence (ICAART 2022), Feb 2022, Online, United States. pp.403-411, ⟨10.5220/0010829500003116⟩


  • Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

    Implementing a Category-Theoretic Framework for Typed Abstract Syntax

    11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), Jan 2022, Philadelphia, PA, United States. ⟨10.1145/3497775.3503678⟩


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

    Leveraging Event-B Theories for Handling Domain Knowledge in Design Models

    7th International Symposium on Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2021), Nov 2021, Beijing, China. pp.40-58, ⟨10.1007/978-3-030-91265-9_3⟩


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

    Event-B Refinement for Continuous Behaviours Approximation

    19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021), Oct 2021, Gold Coast, QLD, Australia. pp.320-336, ⟨10.1007/978-3-030-88885-5_21⟩


  • Conferences articles without published proceedings
  • Neeraj Kumar Singh, Akshay M Fajge, Raju Halder, Md Imran Alam

    Formal Verification and Code Generation for Solidity Smart Contracts

    Rajiv Pandey, Sam Goundar, and Shahnaz Fatima. Distributed Computing to Blockchain: Architecture, Technology, and Applications, pp.332, In press, 978-0323961462


  • Yamine Aït-Ameur, Guillaume Dupont, Ismail Mendil, Dominique Méry, Marc Pantel, Peter Rivière, Neeraj Singh

    Empowering the Event-B Method Using External Theories

    Integrated Formal Methods, 13274, Springer International Publishing, pp.18-35, 2022, Lecture Notes in Computer Science, 978-3-031-07726-5. ⟨10.1007/978-3-031-07727-2_2⟩


  • Jonathan Certes, Benoît Morgan

    Remote attestation of bare-metal microprocessor software: a formally verified security monitor

    Database and Expert Systems Applications – DEXA 2021 Workshops: BIOKDD, IWCFS, MLKgraphs, AI-CARES, ProTime, AISys 2021, Virtual Event, September 27–30, 2021, Proceedings, 1479, Springer International Publishing, pp.42-51, 2021, Communications in Computer and Information Science book series (CCIS), 978-3-030-87100-0. ⟨10.1007/978-3-030-87101-7_5⟩


  • 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⟩


  • 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 Börger on the Occasion of His 75th Birthday, 12750, Springer, pp.1-13, 2021, Lecture Notes in Computer Science, 978-3-030-76020-5. ⟨10.1007/978-3-030-76020-5_1⟩


  • 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⟩


  • 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⟩


  • 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⟩


  • 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⟩


  • Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Albert Sangiovanni-Vincentelli, Werner Damm, Thomas Henzinger, Kim G. Larsen

    Contracts for System Design

    Now Publishers, 12 (2-3), pp.124-400, 2018, Foundations and Trends® in Electronic Design Automation, 978-1-68083-402-4. ⟨10.1561/1000000053⟩


  • Thesis and HDR
    • Xavier Thirioux

      Verifying Embedded Systems

      HDR, Institut National Polytechnique de Toulouse, September 2016.


    • Florent Latombe

      Systematic use of models of concurrency in executable domain-specific modelling languages

      Master’s Thesis, Institut National Polytechnique de Toulouse, July 2016.


    • Guillaume Verdier

      Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes

      Master’s Thesis, Université de Toulouse, March 2016.


    • Régis Spadotti

      Une théorie mécanisée des arbres réguliers en théorie des types dépendants

      Master’s Thesis, Université Paul Sabatier, May 2016.


    • Arnaud Dieumegard

      Formal Guaranties for Safety Critical Code Generation : the Case of Highly Variable Languages

      Master’s Thesis, Institut National Polytechnique de Toulouse, January 2015.


    • Faiez Zalila

      Methods and tools for the integration of formal verification in domain-specific languages

      Master’s Thesis, Institut National Polytechnique de Toulouse, December 2014.


    • Ievgen Ivanov

      Investigation dans des systèmes abstraits avec entrées et sorties comme fonctions partielles de temps

      Master’s Thesis, Université Paul Sabatier, December 2014.

      URL :

    • Nadezhda Baklanova

      Analyse formellement vérifiée des conflits de partage de ressources en Java multi-tâche

      Master’s Thesis, Université Paul Sabatier, December 2014.

      Abstract URL :

    • Hajer Herbegue Bouhachem

      Approche ADL pour la modélisation d’architecture basée sur les contraintes (calcul de WCET)

      Master’s Thesis, Université Paul Sabatier, September 2014.


    • Ning Ge

      Property Driven Verification Framework: Application to Real-Time Property for UML-MARTE Software Designs

      Master’s Thesis, Institut National Polytechnique de Toulouse, May 2014.



    Contracts team

    AcronymeTitreResp. scDébut – fin
    EBRP-EventB-Rodin-Plus autre Enrichissement de EventB et de RODIN Yamine AIT AMEUR
    2020 – 2024
    ICSPA Assistants de preuve basés sur la théorie des ensembles interopéables et sûres Yamine AIT AMEUR
    2020 – 2024
    ProTiPP Proved Timing-Predictable Processors Mamoun FILALI
    Christine ROCHANGE
    2022 – 2026
    [Contract completed]
    autre Méthodes catégoriques et logiques en transformations de modèles Ralph MATTHES
    2012 – 2016
    [Contract completed]
    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
    [Contract completed]
    autre Vérification formelle d’un générateur de code pour un langage synchrone Martin STRECKER
    2010 – 2014
    AcronymeTitreResp. scDébut – fin
    [Contract completed]
    autre Intégration correcte de modèles discrets et continus Neeraj SINGH
    2017 – 2022
    [Contract completed]
    Financement de la préparation du projet SLEVOGT Martin STRECKER
    2017 – 2017
    [Contract completed]
    Méthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques Yamine AIT AMEUR
    2016 – 2021
    [Contract completed]
    Vérification de systèmes distribués paramétrés Philippe QUÉINNEC
    2016 – 2021
    [Contract completed]
    Advanced Multilateral Argumentation for Deliberation Xavier THIRIOUX
    2013 – 2017
    [Contract completed]
    Convention de soutien à un projet rattaché à un chantier : N°RTRA-STAE/2011/BRIEFCASE/06 Marc PANTEL
    2013 – 2014
    [Contract completed]
    Integration des semantique implicite et explicite dans le développement de systèmes discrets fondés sur la panne Yamine AIT AMEUR
    2013 – 2017
    [Contract completed]
    Plateforme avionique modulaire etendue Yamine AIT AMEUR
    2013 – 2015
    [Contract completed]
    Vérification des optimisations rapides appliquées à la commande embarquée Marc PANTEL
    2013 – 2016
    AcronymeTitreResp. scDébut – fin
    Friday 3 December 2021, 14h00
    Development of a Formal Verification Methodology for B specifications using PERF toolkit. Application to safety requirements of railway systems
    Alexandra HALCHIN – Team ACADIE, IRIT INP-ENSEEIHT, Salle du Conseil (F501)
    Thursday 14 January 2021, 15h00
    Correct-by-Construction Design of Hybrid Systems Based on Refinement and Proof
    Guillaume DUPONT – Team ACADIE, IRIT INP-ENSEEIHT, En visioconférence
    Monday 14 September 2020, 10h00
    Un environnement formel pour la sémantique des systèmes hétérogènes
    Mathieu MONTIN – Team ACADIE, IRIT INP-ENSEEIHT, Auditorium et via visioconférence
    Friday 12 June 2020, 14h00
    Semantic transformations for the evolution of data models
    Lynda AIT OUBELLI – Team ACADIE, IRIT INP-ENSEEIHT, En visioconférence
    Tuesday 15 October 2019, 14h00
    Sur le pouvoir expressif des structures applicatives et monadiques indexées
    Ian MALAKHOVSKI – Team ACADIE, IRIT UT3 Paul Sabatier, IRIT, Salle 001
    Friday 15 December 2017, 9h00
    Formal decomposition of Event-B centralized specifications: application to BIP distributed systems
    Badr SIALA – Team ACADIE – IRIT UT3 Paul Sabatier, IRIT, Salle des Thèses
    Wednesday 22 November 2017, 10h15
    Formalisation of Asynchronous Interactions
    Florent CHEVROU – Team ACADIE – IRIT INP-ENSEEIHT, Salle des thèses
    Thursday 6 July 2017, 9h30
    A formal approach for correct-by-construction system substitution
    Guillaume BABIN – Team ACADIE – IRIT ENSEEIHT, Amphi A001
    Wednesday 5 July 2017, 9h30
    Modular avionics software integration on multicore COTS: certification-compliant methodology and timing analysis metrics for legacy software reuse…
    Soukayna M’SIRDI – Team ACADIE – IRIT ENSEEIHT, Amphi A001
    Wednesday 13 July 2016, 11h00
    Systematic Use of Models of Concurrency in eXecutable Domain-Specific Modeling Languages
    Florent LATOMBE – Team ACADIE – IRIT Salle du Conseil, F501
    Monday 28 October 2019 – Thursday 31 October 2019
    MEDI 2019 : 9th International Conference on Model and Data Engineering
    #congres Know more
    Monday 26 June 2017 – Friday 30 June 2017
    École Jeunes Chercheurs en Programmation 2017 (EJCP 2017)
    INP-ENSEEIHT, Toulouse
    #congres Know more
    Monday 12 December 2016 – Friday 16 December 2016
    World Champions Programming School at Toulouse
    UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
    #congres Know more
    Wednesday 18 June 2014 – Friday 20 June 2014
    LACL 2014 : Logical Aspects of Computational Linguistics
    UT3 Paul Sabatier, IRIT
    #congres Know more
    Monday 2 June 2014 – Thursday 5 June 2014
    ABZ 2014 : 4th International Conference ASM, Alloy, B, TLA, VDM, Z
    #congres Know more
    Thursday 27 February 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
    Thursday 26 September 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
    Wednesday 29 May 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
    Friday 16 February 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
    Tuesday 21 February 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
    Tuesday 10 January 2017, 14h00 – 15h30
    A new dimension of Cloud Governance
    Ernesto PIMENTEL – Université de Malaga (Espagne) INP-ENSEEIHT, Salle des thèses
    Monday 12 December 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
    Tuesday 2 September 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
    Thursday 23 January 2014, 14h00
    From MTL to deterimistic timed automata
    Dejan NICKOVIC – Austrian Institute of Technology (Autriche) UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
    Friday 6 July 2018, 9h30
    Formalisations pour les compositions de services
    Aurélie HURAULT – Team ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
    Monday 19 September 2016, 9h30
    Verifying Embedded Systems
    Xavier THIRIOUX – Team ACADIE – IRIT INP-ENSEEIHT, Salle des theses
    Thursday 25 June 2015
    Journée du GDR GPL – Génie Logiciel et Transfert Technologique
    UT3 Paul Sabatier, IRIT
    Wednesday 22 April 2015 – Thursday 23 April 2015
    Journées FAC’2015 : Formalisation des Activités Concurrentes
    INP-ENSEEIHT, Salle des theses