ACADIE Team

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…

skills

Formal methods
Verification and validation
Proof environments
Critical systems
Modelling

Members team

Permanent members
Non-permanent members
Related members

publications team

International journals articles
  • 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

  • National journals articles
    Special issues of journal
    International conferences articles
  • 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

  • National conferences articles
  • 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

  • Conferences articles without published proceedings
    Books
  • Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel, Neeraj Singh

    Event-B Refinement for Continuous Behaviours Approximation

    Automated Technology for Verification and Analysis, 12971, Springer International Publishing, pp.320-336, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-88885-5_21⟩

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

  • 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

  • Books Books edition Books parts
    Thesis and HDR
  • 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

  • Thesis and HDR
    • Xavier Thirioux

      Verifying Embedded Systems

      HDR, Institut National Polytechnique de Toulouse, September 2016.

      BibTeX

    • Florent Latombe

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

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

      BibTeX

    • Guillaume Verdier

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

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

      BibTeX

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

      Abstract
      BibTeX

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

      BibTeX

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

      BibTeX

    • 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 : http://www.theses.fr/en/2014TOU30022
      BibTeX

    • 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 : http://www.irit.fr/publis/ACADIE/main.pdf
      BibTeX

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

      BibTeX

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

      BibTeX

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

  • Reports

    Contracts team

    AcronymeTitreResp. scDébut – fin
    DISCONT anr Intégration correcte de modèles discrets et continus Neeraj SINGH
    2017 – 2022
    EventB-Rodin-Plus – EBRP-EventB-Rodin-Plus anr Enrichissement de EventB et de RODIN : EventB-Rodin-Plus – EBRP-EventB-Rodin-Plus Yamine AIT AMEUR
    2019 – 2023
    FORMEDICIS
    [Contract completed]
    anr Méthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques Yamine AIT AMEUR
    2016 – 2021
    PARDI
    [Contract completed]
    anr Vérification de systèmes distribués paramétrés Philippe QUéINNEC
    2016 – 2021
    IMPEX
    [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
    VORACE
    [Contract completed]
    anr Vérification des optimisations rapides appliquées à la commande embarquée Marc PANTEL
    2013 – 2016
    CLIMT
    [Contract completed]
    autre Méthodes catégoriques et logiques en transformations de modèles Ralph MATTHES
    2012 – 2016
    GeMoC
    [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
    Verisync
    [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
    OPEES
    [Contract completed]
    autre Plateforme ouverte pour ingénierie des systèmes embarqués Marc PANTEL
    2009 – 2012
    AcronymeTitreResp. scDébut – fin
    INP2011-003
    [Contract completed]
    Modélisation des dépendances entre fonctions de niveau avion pour l’analyse des risques Yamine AIT AMEUR
    2011 – 2012
    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
    #these
    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
    #these
    Friday 12 June 2020, 14h00
    Semantic transformations for the evolution of data models
    Lynda AIT OUBELLI – Team ACADIE, IRIT INP-ENSEEIHT, En visioconférence
    #these
    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
    #these
    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
    #these
    Wednesday 22 November 2017, 10h15
    Formalisation of Asynchronous Interactions
    Florent CHEVROU – Team ACADIE – IRIT INP-ENSEEIHT, Salle des thèses
    #these
    Thursday 6 July 2017, 9h30
    A formal approach for correct-by-construction system substitution
    Guillaume BABIN – Team ACADIE – IRIT ENSEEIHT, Amphi A001
    #these
    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
    #these
    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
    #these
    Thursday 19 May 2016, 10h00
    Une théorie mécanisée des arbres réguliers en théorie des types dépendants
    Régis SPADOTTI – Team ACADIE – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
    #these
    Monday 28 October 2019 – Thursday 31 October 2019
    MEDI 2019 : 9th International Conference on Model and Data Engineering
    INP-ENSEEIHT
    #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
    Toulouse
    #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
    #seminaire
    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
    #seminaire
    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
    #seminaire
    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
    #seminaire
    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
    #seminaire
    Tuesday 10 January 2017, 14h00 – 15h30
    A new dimension of Cloud Governance
    Ernesto PIMENTEL – Université de Malaga (Espagne) INP-ENSEEIHT, Salle des thèses
    #seminaire
    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
    #seminaire
    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
    #seminaire
    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
    #seminaire
    Friday 6 July 2018, 9h30
    Formalisations pour les compositions de services
    Aurélie HURAULT – Team ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
    #hdr
    Monday 19 September 2016, 9h30
    Verifying Embedded Systems
    Xavier THIRIOUX – Team ACADIE – IRIT INP-ENSEEIHT, Salle des theses
    #hdr
    Thursday 25 June 2015
    Journée du GDR GPL – Génie Logiciel et Transfert Technologique
    UT3 Paul Sabatier, IRIT
    #journee
    Wednesday 22 April 2015 – Thursday 23 April 2015
    Journées FAC’2015 : Formalisation des Activités Concurrentes
    INP-ENSEEIHT, Salle des theses
    #journee