Equipe ACADIE

Responsable : Jan-Georg SMAUS

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
Théorie des jeux

personnel de l’équipe

Membres permanents
Membres non – permanents
Membres extérieur

publications de l’équipe

Articles dans des revues internationales
  • Albert Benveniste, Jean-Baptiste Raclet

    Mixed Nondeterministic-Probabilistic Automata

    Discrete Event Dynamic Systems, 2023, 2023, pp.1-58. ⟨10.1007/s10626-023-00375-x⟩

    Accès: https://ut3-toulouseinp.hal.science/hal-04276789v1

  • Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux

    Enabling Floating-Point Arithmetic in the Coq Proof Assistant

    Journal of Automated Reasoning, 2023, 67 (33), ⟨10.1007/s10817-023-09679-x⟩

    Accès: https://inria.hal.science/hal-04114233v2

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

    Accès: https://hal.science/hal-04086420v1

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

    Accès: https://hal.science/hal-03617603v1

  • 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, 20 (4), pp.168-180. ⟨10.2514/1.I011093⟩

    Accès: https://hal.science/hal-04027880v1

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

    Accès: https://inria.hal.science/hal-03904803v1

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

    Accès: https://ut3-toulouseinp.hal.science/hal-03658700v2

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

    Accès: https://hal.science/hal-03836811v1

  • Guillaume Dupont, Yamine Aït-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⟩

    Accès: https://hal.science/hal-03513847v1

  • 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/j.is.2021.101765⟩

    Accès: https://hal.science/hal-03170863v1

  • Articles dans des revues nationales
  • 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⟩

    Accès: https://hal.science/hal-03617760v1

  • Articles dans des revues nationales
    Rédaction de numéros spéciaux de revues
  • Ladjel Bellatreche, Yamine Aït-Ameur, George Angelos Papadopoulos

    Models and Data Engineering

    Future Generation Computer Systems, 68, 2017, Models and data engineering, ⟨10.1016/j.future.2016.11.017⟩

    Accès: https://hal.science/hal-03128351v1

  • Rédaction de numéros spéciaux de revues
    Conférences et workshops internationaux avec actes édités et comité de lecture
  • Ralph Matthes, Kobe Wullaert, Benedikt Ahrens

    Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories

    9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Jul 2024, Tallinn, Estonia. pp.25:1-25:22, ⟨10.4230/LIPIcs.FSCD.2024.25⟩

    Accès: https://hal.science/hal-04642448v1

  • Jean-Paul Bodeveix, Thomas Carle, Elie Fares, Mamoun Filali, Thai Son Hoang

    Verifying HyperLTL properties in Event-B

    10th International Conference on Rigorous State-Based Methods (ABZ 2024), Jun 2024, Bergame, Italy. pp.255-261, ⟨10.1007/978-3-031-63790-2_20⟩

    Accès: https://hal.science/hal-04662665v1

  • Anne Grieu

    From Event-B to Lambdapi

    10th International Conference on Rigourous State-Based Methods (ABZ 2024), ABZ, Jun 2024, Bergamo, Italy. pp.387-391, ⟨10.1007/978-3-031-63790-2_29⟩

    Accès: https://ut3-toulouseinp.hal.science/hal-04691826v1

  • Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert

    Displayed Monoidal Categories for the Semantics of Linear Logic

    CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2024, London, United Kingdom. pp.260-273, ⟨10.1145/3636501.3636956⟩

    Accès: https://hal.science/hal-04375376v1

  • Mika Pons, Jean-Michel Bruel, Jean-Baptiste Raclet, Franck Silvestre

    Traceability by design: design of an interactive system to improve the automatic generation of Git traces during a learning activity

    18th European Conference on Technology Enhanced Learning (EC-TEL 2023), Sep 2023, Aveiro, Portugal. pp.611-617, ⟨10.1007/978-3-031-42682-7_50⟩

    Accès: https://hal.science/hal-04347305v1

  • Denis Ollivier, Franck Silvestre, Jean-Baptiste Raclet, Emmanuel Lescure, Julien Broisin

    Designing a Revision System: An Exploratory Qualitative Study to Identify the Needs of French Teachers and Students

    18th European Conference on Technology-Enhanced Learning (EC-TEL 2023), European Association of Technology-Enhanced Learning, Sep 2023, Aveiro, Portugal. pp.294-307, ⟨10.1007/978-3-031-42682-7_20⟩

    Accès: https://hal.science/hal-04211163v1

  • 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, ⟨10.4230/LIPIcs.ITP.2023.12⟩

    Accès: https://telecom-paris.hal.science/hal-04098856v2

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

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

    14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Bialystok, Poland. ⟨10.4230/LIPICS.ITP.2023.25⟩

    Accès: https://hal.science/hal-04269882v1

  • Aurélie Hurault, Joao Marques-Silva

    Certified Logic-Based Explainable AI

    17th International Conference on Tests and Proofs (TAP 2023), Jul 2023, Leicester, United Kingdom. pp.51-67, ⟨10.1007/978-3-031-38828-6_4⟩

    Accès: https://hal.science/hal-04031193v3

  • Mika Pons, Jean-Michel Bruel, Jean-Baptiste Raclet, Franck Silvestre

    Traçabilité by design : conception d’un système interactif pour améliorer la génération automatique de traces Git pendant une activité d’apprentissage

    11ème Conférence sur les Environnements Informatiques pour l’Apprentissage Humain (EIAH 2023), ATIEF : Association des Technologies de l’Information pour l’Education et la Formation, Jun 2023, Brest, France. pp.68-79

    Accès: https://hal.science/hal-04144980v1

  • Conférences et workshops nationaux avec actes édités et comité de lecture
  • Anne Grieu

    From Event-B to Lambdapi (Journées FAC 2024)

    FAC 2024, groupe IFSE du RTRA STAE, Apr 2024, Toulouse, France

    Accès: https://ut3-toulouseinp.hal.science/hal-04692230v1

  • Denis Ollivier, Franck Silvestre, Jean-Baptiste Raclet, Emmanuel Lescure, Julien Broisin

    Conception d’un système de révisions : une étude qualitative exploratoire pour identifier les besoins des enseignants et des élèves

    11ème Conférence sur les Environnements Informatiques pour l’Apprentissage Humain (EIAH 2023), ATIEF : Association des Technologies de l’Information pour l’Education et la Formation, Jun 2023, Brest, France. pp.36-41

    Accès: https://hal.science/hal-04164903v1

  • 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 (EJCIM 2022), GDR Informatique Mathématique, Jun 2022, Nice, France

    Accès: https://hal.science/hal-03709703v1

  • 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.science/hal-03298722v1

  • Érik Martin-Dorel, Pierre Roux

    Flottants primitifs dans Coq

    32èmes Journées Francophones des langages applicatifs (JFLA 2021), Apr 2021, virtuel, France

    Accès: https://hal.science/hal-03463839v1

  • Jean-Baptiste Raclet, Franck Silvestre, Mika Pons

    Mise en oeuvre d’approches pédagogiques fondées sur des pratiques de l’industrie du logiciel pour l’apprentissage de la programmation

    8ème Colloque Didapro : L’informatique, objets d’enseignements (DidaSTIC 2020), Feb 2020, Lille, France. pp.1-12

    Accès: https://hal.science/hal-02960444v1

  • 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.science/hal-02442015v1

  • 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.science/hal-02930097v1

  • Conférences sans actes publiés
    Livres (monographies)
  • Neeraj Kumar Singh, Akshay M Fajge, Raju Halder, Md. Imran Alam

    Formal Verification and Code Generation for Solidity Smart Contracts

    Rajiv Pandey; Sam Goundar; Shahnaz Fatima. Distributed Computing to Blockchain: Architecture, Technology, and Applications, Elsevier, pp.125-144, 2023, 978-0323961462. ⟨10.1016/B978-0-323-96146-2.00028-0⟩

    Accès: https://hal.science/hal-04019340v1

  • Yamine Aït-Ameur, Ismail Mendil, Guillaume Dupont, Dominique Méry, Marc Pantel, Peter Riviere, Neeraj Kumar 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⟩

    Accès: https://inria.hal.science/hal-03904799v1

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

    Accès: https://hal.science/hal-03576711v1

  • 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.science/hal-03255968v1

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

    Accès: https://inria.hal.science/hal-03250787v1

  • 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://inria.hal.science/hal-03199742v1

  • 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://inria.hal.science/hal-02910199v1

  • 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.science/hal-02365814v1

  • 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.science/hal-02360681v1

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

    Accès: https://inria.hal.science/hal-01971429v1

  • Recueils des communications
  • Kobe Wullaert, Ralph Matthes, Benedikt Ahrens

    Univalent Monoidal Categories

    Leibniz International Proceedings in Informatics , 269, Schloss Dagstuhl – Leibniz Center for Informatics, pp.15:1-15:21, 2023, 28th International Conference on Types for Proofs and Programs (TYPES 2022), 978-3-95977-285-3. ⟨10.4230/LIPIcs.TYPES.2022.15⟩

    Accès: https://hal.science/hal-03889672v1

  • Philippe Cuenot, Marie de Roquemaurel, Kevin Delmas, Jean-Marc Gabriel, Adrien Gauffriau, Christophe Grand, Éric Jenn, Mohamed Kaâniche, Benoît Morgan

    ERTS 2022 proceedings

    2022

    Accès: https://hal.science/hal-03704287v1

  • Rédaction d'actes de conférences et de workshops
    Thèses et habilitations
  • Neeraj Kumar Singh

    Rigorous Safety-Critical Cyber-Physical Systems Development using Formal Methods

    Computer Science [cs]. Toulouse INP, 2024

    Accès: https://hal.science/tel-04695651v1

  • Peter Riviere

    Automatic generation of proof obligations parameterised by domain theories implementation in Event-B : The EB4EB Framework

    Computer Science [cs]. Université de Toulouse, 2024. English. ⟨NNT : 2024TLSEP052⟩

    Accès: https://theses.hal.science/tel-04677532v1

  • Jonathan Certes

    Méthodes et modèles pour la vérification formelle de l’attestation à distance sur microprocesseur

    Sciences de l’information et de la communication. Université Paul Sabatier – Toulouse III, 2023. Français. ⟨NNT : 2023TOU30168⟩

    Accès: https://theses.hal.science/tel-04349901v1

  • Jonathan Certes

    Méthodes et modèles pour la vérification formelle de l’attestation à distance sur microprocesseur

    Informatique [cs]. Université Toulouse 3 – Paul Sabatier, 2023. Français. ⟨NNT : ⟩

    Accès: https://hal.science/tel-04457569v1

  • Alexandra Halchin

    Development of a Formal Verification Methodology for B Specifications using PERF formal toolkit. Application to safety requirements of railway systems.

    Other [cs.OH]. Institut National Polytechnique de Toulouse – INPT, 2021. English. ⟨NNT : 2021INPT0118⟩

    Accès: https://theses.hal.science/tel-04186724v1

  • Maksim Kalameyets

    Algorithms and techniques for bot detection in social networks

    Library and information sciences. Université Paul Sabatier – Toulouse III; ITMO University, 2021. English. ⟨NNT : 2021TOU30097⟩

    Accès: https://theses.hal.science/tel-03560882v1

  • Guillaume Dupont

    Correct-by-Construction Design of Hybrid Systems Based on Refinement and Proof

    Other [cs.OH]. Institut National Polytechnique de Toulouse – INPT, 2021. English. ⟨NNT : 2021INPT0001⟩

    Accès: https://theses.hal.science/tel-04165215v1

  • 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. ⟨NNT : ⟩

    Accès: https://hal.science/tel-03123969v1

  • Mathieu Montin

    A formal framework for heterogeneous systems semantics

    Networking and Internet Architecture [cs.NI]. Institut National Polytechnique de Toulouse – INPT, 2020. English. ⟨NNT : 2020INPT0072⟩

    Accès: https://theses.hal.science/tel-04169893v1

  • 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://theses.hal.science/tel-02735749v1

  • Rapports
  • Albert Benveniste, Jean-Baptiste Raclet

    Mixed Nondeterministic-Probabilistic Automata: Blending graphical probabilistic models with nondeterminism

    [Research Report] RR-9447, Inria Rennes – Bretagne Atlantique. 2022, pp.1-52

    Accès: https://inria.hal.science/hal-03531059v1

  • Albert Benveniste, Kim G 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://inria.hal.science/hal-02985273v1

  • Xavier Thirioux, Alexis Maffart

    Taylor Series Revisited

    ISAE/DISC/RT2020/1, Institut Supérieur de l’Aéronautique et de l’Espace. 2020

    Accès: https://hal.science/hal-04357221v1

  • É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.science/hal-03109258v1

  • Rapports

    contrats de l’équipe

    AcronymeTitreCadre FinancementResp. scDébut
    europa
    AcronymeTitreCadre FinancementResp. scDébut
    EBRP-EventB-Rodin-Plus Enrichissement de EventB et de RODIN

    Appels à projets ANR (hors PIA) Yamine AIT AMEUR
    2020
    Learn OCaml 2022-2026Convention de financement pour l’accueil d’étudiants stagiaires LearnOCaml 2022-2026

    Fondations, associations, mécénats Erik MARTIN-DOREL
    2022
    ProTiPP Proved Timing-Predictable Processors

    Appels à projets ANR (hors PIA)
    Christine ROCHANGE
    2023
    ForML – Toulouse INP Raisonnements formellement certifiés en apprentissage automatique – Toulouse INP

    Appels à projets ANR (hors PIA) André-Luc BEYLOT
    Aurélie HURAULT
    2024
    Learn OCaml 2021
    [Contrat terminé]
    Learn OCaml 2021

    Fondations, associations, mécénats Erik MARTIN-DOREL
    2021
    ICSPA
    [Contrat terminé]
    Assistants de preuve basés sur la théorie des ensembles interopéables et sûres

    Appels à projets ANR (hors PIA) Yamine AIT AMEUR
    2020
    Learn OCaml 2020
    [Contrat terminé]
    Learn OCaml 2020

    Fondations, associations, mécénats Erik MARTIN-DOREL
    2020
    Learn OCaml 2019
    [Contrat terminé]
    Learn OCaml 2019

    Fondations, associations, mécénats Erik MARTIN-DOREL
    2019
    DISCONT
    [Contrat terminé]
    Intégration correcte de modèles discrets et continus

    Appels à projets ANR (hors PIA) Neeraj SINGH
    2017
    Slevogt
    [Contrat terminé]
    Financement de la préparation du projet SLEVOGT

    Autres financements publics sur appel à projets Martin STRECKER
    2017
    FORMEDICIS
    [Contrat terminé]
    Méthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques

    Appels à projets ANR (hors PIA) Yamine AIT AMEUR
    2016
    PARDI
    [Contrat terminé]
    Vérification de systèmes distribués paramétrés

    Appels à projets ANR (hors PIA) Philippe QUÉINNEC
    2016
    [Contrat terminé]Ingénierie formelle des systèmes embarqués

    Fondations, associations, mécénats Marc PANTEL
    2016
    AMANDE
    [Contrat terminé]
    Advanced Multilateral Argumentation for Deliberation

    Appels à projets ANR (hors PIA)
    2013
    BRIEFCASE
    [Contrat terminé]
    Convention de soutien à un projet rattaché à un chantier : N°RTRA-STAE/2011/BRIEFCASE/06

    Fondations, associations, mécénats Marc PANTEL
    2013
    IMPEX
    [Contrat terminé]
    Integration des semantique implicite et explicite dans le développement de systèmes discrets fondés sur la panne

    Appels à projets ANR (hors PIA) Yamine AIT AMEUR
    2013
    PANDA
    [Contrat terminé]
    Plateforme avionique modulaire etendue

    Programme d’Investissements d’Avenir (PIA) Yamine AIT AMEUR
    2013
    VORACE
    [Contrat terminé]
    Vérification des optimisations rapides appliquées à la commande embarquée

    Appels à projets ANR (hors PIA) Marc PANTEL
    2013
    anr anr
    AcronymeTitreCadre FinancementResp. scDébut
    europa
    Vendredi 7 Juin 2024, 10h00
    Génération automatique d’obligations de preuves paramétrée par des théories de domaine dans Event-B : Le cadre de travail EB4EB
    Peter RIVIERE – Equipe ACADIE, IRIT Toulouse INP-ENSEEIHT, Salle des thèses C002
    #these
    Lundi 18 Décembre 2023, 10h00
    Décision individuelle et stratégique sous incertitude : une approche algébrique et formelle
    Pierre POMERET-COQUOT – Equipe ADRIA, Equipe ACADIE, IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
    #these
    Jeudi 5 Octobre 2023, 14h00
    Un cadre formel pour la modélisation explicite des connaissances de domaine dans les méthodes formelles orientées états : application à des systèmes critiques interactifs
    Ismail MENDIL – Equipe ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
    #these
    Jeudi 22 Juin 2023, 14h00
    Méthodes et modèles pour la vérification formelle de l’attestation à distance sur microprocesseur
    Jonathan CERTES – Equipe ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
    #these
    Vendredi 3 Décembre 2021, 14h00
    Development of a Formal Verification Methodology for B specifications using PERF toolkit. Application to safety requirements of railway systems
    Alexandra HALCHIN – Equipe ACADIE, IRIT INP-ENSEEIHT, Salle du Conseil (F501)
    #these
    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
    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
    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
    Vendredi 21 Juin 2024, 10h00
    Rigorous Safety-Critical Cyber-Physical Systems Development using Formal Methods
    Neeraj SINGH – Equipe ACADIE, IRIT Toulouse INP-ENSEEIHT, Salle des thèses C002
    #hdr
    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