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
personnel de l’équipe
- Yamine AIT AMEURProfesseur – Toulouse INP
- Jean-Paul BODEVEIXProfesseur – UT3
- Christelle CHAUDETMaître de Conférences – UT3
- Xavier CRÉGUTMaître de Conférences – Toulouse INP
- Guillaume DUPONTMaître de Conférences – Toulouse INP
- Aurélie HURAULTProfesseur – Toulouse INP
- Erik MARTIN-DORELMaître de Conférences – UT3
- Ralph MATTHESChargé de Recherche (HDR) – CNRS
- Stefan NEUWIRTHMaître de Conférences (HDR) – Université de Franche-Comté
- Meriem OUEDERNIMaître de Conférences – Toulouse INP
- Marc PANTELMaître de Conférences – Toulouse INP
- Quentin PEYRASMaître de Conférences – UT3
- Philippe QUÉINNECProfesseur – Toulouse INP
- Jean-Baptiste RACLETMaître de Conférences – UT3
- Neeraj SINGHMaître de Conférences (HDR) – Toulouse INP
- Jan-Georg SMAUSProfesseur – UT3
- Sergei SOLOVIEVProfesseur – UT3
- Martin STRECKERMaître de Conférences – UT3
- Yannis BENABBIDoctorant – Toulouse INP
- Imane BOUSDIRADoctorant – Toulouse INP (co-encadrement ADRIA)
- Christophe CHENDoctorant – Toulouse INP
- Rosalie DEFOURNÉChercheur Contractuel – UT3 (co-encadrement ADRIA)
- Alexandre DUBOISEnseignant-chercheur MAST – UT3
- Anne GRIEUDoctorant – Toulouse INP
- Mika PONSDoctorant – UT Capitole (co-encadrement SMART, TALENT)
- Khadidja SALAH MANSOUREnseignant-chercheur ATER – UT3
- Guillaume VERDIERIngénieur de Recherche – Autre tutelle
- Elie FARESEnseignant-chercheur Associé – Ras al Khaimah – UAE
- Benoit MORGANEnseignant-chercheur Associé – Autre
- Peter RIVIEREJeune docteur IRIT – Toulouse INP
- Gaziza YELIBAYEVAEnseignant-chercheur Invité – Kazakhstan
publications de l’équipe
Albert Benveniste, Jean-Baptiste Raclet
Mixed Nondeterministic-Probabilistic Automata
Discrete Event Dynamic Systems, 2023, 2023, pp.1-58. ⟨10.1007/s10626-023-00375-x⟩
É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⟩
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⟩
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⟩
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⟩
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 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⟩
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⟩
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⟩
Yang Zhibin, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu
Towards a verified compiler prototype for the synchronous language SIGNAL
Dans : Frontiers of Computer Science, Springer, Vol. 10, N. 1, p. 37-53, février 2016.
Zhibin Yang, Kai Hu, Yongwang Zhao, Dianfu Ma, Jean-Paul Bodeveix
AADL Model Verification by Translating into TASM
Dans : Journal of Software, Institute of Software Chinese Academy of Science (ISCAS), China, Vol. 26, N. 2, p. 1-20, février 2015.
Aurélie Hurault, Marc Pantel, Michel Daydé
Composition automatique de services de calcul – Utilisation des spécifications algébriques pour décrire la fonctionnalité des services
Dans : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Numéro spécial La composition d’objets, de composants et de services, Vol. 30, N. 6/2011, p. 685-710, juin 2011.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
Expérimentations en Coq pour un générateur de code qualifiable
Dans : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Numéro spécial Méthodes formelles à l’analyse et la compilation, Vol. 30, N. 4/2011, p. 409-440, avril 2011.
Zhibin Yang, Lei Pi, Kai Hu, Zong-Hua Gu, Dianfu Ma
AADL: an Architecture Design and Analysis Language for Complex Embedded Real-time Systems
Dans : Journal of Software, Institute of Software Chinese Academy of Science (ISCAS), China, Vol. 21, N. 5, p. 899-915, mai 2010.
Accès : http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3700&flag=1
BibTeXAngel Garcia, Benoit Combemale, Xavier Crégut, Jérôme Vandeur
TopPROCESS : vers une ingénierie des procédés dirigée par les modèles
Dans : Revue de l’Electricité et de l’Electronique (REE), Société de l’Electricité, de l’Electronique et des Technologies de l’Information et de la Communication (SEE), Paris, Vol. 2009, N. 2, p. 31-37, février 2009.
Odile Nasr, Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali
Spécification et vérification d’un ordonnanceur en B via les automates temporisés
Dans : L’Objet, Hermès Science, Numéro spécial Composants, services et aspects techniques et outils pour la vérification, Vol. 14, N. 4, p. 43-72, décembre 2008.
Olga Antonova, Sergei Soloviev
Le test de Turing et la question d’une definition de la realite virtuelle
Dans : Logiko-philosophskie shtudii. (Etudes logiko-philosophiques), Universite d’Etat de St. Petersbourg, Russia, Vol. 5, p. 50-67, 2008.
Benoit Combemale, Xavier Crégut, Pierre Michel, Marc Pantel
SéMo’07 : premier atelier sur la Sémantique des Modèles
Dans : L’Objet, Hermès Science, Numéro spécial Ingénierie Dirigée par les Modèles, Vol. 13, N. 4, p. 137-144, janvier 2008.
Olga Antonova, Sergei Soloviev
Axiomatika i ochevidnost. (Axiomatique et evidence.)Logiko-philosophskie shtudii, 4, Universite d’Etat de St. Petersbourg
Dans : Logiko-philosophskie shtudii. (Etudes logiko-philosophiques), Universite d’Etat de St. Petersbourg, Russia, Vol. 4, p. 3-11, août 2007.
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⟩
Yamine Ait Ameur, Klaus-Dieter Schewe
Introduction to the ABZ 2014 special issue
Dans : Science of Computer Programming, Elsevier, Vol. 131, 2016.
Ladjel Bellatreche, Yamine Ait Ameur, Anne Monceaux
Editorial
Dans : Computers in Industry, Elsevier, Vol. 65 N. 9, 2014.
Special Issue “Sixth Workshop on Fixed Points in Computer Science, FICS 2009”
Dans : RAIRO – Theoretical Informatics and Applications, EDP Sciences, Vol. 47 N. 1, 2013.
Ralph Matthes, Sergei Soloviev
CAMCAD ’09 Commutativity of Algebraic Diagrams
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 22 N. 6, décembre 2012.
Accès : http://journals.cambridge.org/action/displayIssue?jid=MSC&volumeId=22&seriesId=0&issueId=06
BibTeXRalph Matthes, Sergei Soloviev
Isomorphism of types and invertibility of lambda terms
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 18, août 2008.
Sergei Soloviev, Roberto Di Cosmo
Isomorphism of Types
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 15 N. 5, octobre 2005.
Jean-Paul Arcangeli, Mamoun Filali, Abdelkader Hameurlain, Gérard Padiou
Les environnements d’exécution répartie
Dans : Calculateurs Parallèles, Réseaux et Systèmes Répartis, HERMES, 8, quai du Marche-Neuf 75004 Paris France, Vol. 10, 5, 1998.
Jean-Paul Bodeveix, Christian Percebois, Salam Majoul
Coordinating Objects through Multiset Rewriting
Dans : Special Issues in Object-Oriented Programming, Mühlhäuser, Vol. 3, mars 1997.
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⟩
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⟩
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⟩
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⟩
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⟩
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⟩
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⟩
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⟩
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⟩
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
From Event-B to Lambdapi (Journées FAC 2024)
FAC 2024, groupe IFSE du RTRA STAE, Apr 2024, Toulouse, France
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
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
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
Érik Martin-Dorel, Pierre Roux
Flottants primitifs dans Coq
32èmes Journées Francophones des langages applicatifs (JFLA 2021), Apr 2021, virtuel, France
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
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
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⟩
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, Mamoun Filali
An Event-B development process for the distributed BIP framework
Dans : FAC, Toulouse, 30/03/16-31/03/16.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
Dans : Journées FAC 2016, LAAS, Toulouse, 30/03/16-31/03/16.
Accès : http://projects.laas.fr/IFSE/FAC/previous/journ%C3%A9es-fac-2016/
BibTeXErik Martin-Dorel, Guillaume Melquiond
CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq
Dans : The MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, CIRM, Luminy, Marseille, 11/01/16-15/01/16.
Accès : http://scientific-events.weebly.com/1508.html
BibTeXFormal proofs and certified computation in Coq
Dans : The French Symposium on Games – Theory and Applications, Université Paris Diderot, 26/05/15-30/05/15.
Ning Ge, Marc Pantel, Xavier Crégut
Probabilistic Failure Analysis in Model Validation & Verification
Dans : Formalisation des Activités Concurrentes, Toulouse, 16/04/14-17/04/14.
Evgeny Dantsin, Jan-Georg Smaus, Sergei Soloviev
Algorithms in Games Evolving in Time: Winning Strategies Based on Testing Hypotheses
Dans : Isabelle Users Workshop of the International Conference on Interactive Theorem Proving, Princeton, USA, 12/08/12-12/08/12, Tobias Nipkow, Larry Paulson, Makarius Wenzel (Eds.).
Transactional Memory Protocols for Multicore Processors
Dans : CONAIS 2012 (9o Congreso Nacional y 6o Internacional de Informática y Sistemas), Villahermosa (Mexique), 19/09/12-21/09/12 (conférencier invité).
Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann
Implementations of two algorithms for the threshold synthesis problem
Dans : International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, 09/01/12-11/01/12 (conférencier invité).
Résumé Accès : http://www.cs.uic.edu/pub/Isaim2012/WebPreferences/ISAIM2012_Boolean_Schilling_etal.pdf
BibTeXUnivariate and Bivariate Integral Roots Certificates Based on Hensel Lifting
Dans : The Third Coq Workshop 2011, Nijmegen, Netherlands, 26/08/11-26/08/11, Bas Spitters (Eds.).
Accès : http://www.cs.ru.nl/~spitters/coqw_files/program.html
BibTeXElie Fares, Jean-Paul Bodeveix, Mamoun Filali
A Transformation and Verification Framework for BPEL
Dans : Services et Langages et modèles à l’exécution, LILLE GDR GPL, 10/06/11-10/06/11.
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⟩
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⟩
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⟩
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⟩
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⟩
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⟩
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⟩
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
Ladjel Bellatreche, Oscar Pastor, Jesus Almendros-Jimenez, Yamine Ait Ameur
Model and Data Engineering – 6th International Conference, MEDI 2016, Almeria,, 21/09/16 – 23/09/16, Springer-Verlag, LNCS 9893, septembre 2016.
Tenth International Workshop on Fixed Points in Computer Science (FICS 2015), Berlin, Allemagne, 11/09/15 – 12/09/15, Electronic Proceedings in Theoretical Computer Science (EPTCS), septembre 2015.
Yamine Ait Ameur, Ladjel Bellatreche, George Angelos Papadopoulos
Model and Data Engineering – 4th International Conference, MEDI 2014, Larnaca, Chypre, 24/09/14 – 26/09/14, Springer-Verlag, LNCS 8748, septembre 2014.
Yamine Ait Ameur, Klaus-Dieter Schewe
Abstract State Machines, Alloy, B, TLA, VDM, and Z – 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings., Toulouse, 02/06/14 – 06/06/14, Springer-Verlag, LNCS 8477, juin 2014.
Ralph Matthes, Aleksy Schubert
19th International Conference on Types for Proofs and Programs (TYPES 2013), Toulouse, 22/04/13 – 26/04/13, Dagstuhl Publishing, Leibniz International Proceedings in Informatics (LIPIcs) 26, juillet 2014.
Accès : http://www.dagstuhl.de/dagpub/978-3-939897-72-9/
BibTeXNicholas Asher, Sergei Soloviev
Logical Aspects of Computational Linguistics, IRIT, Toulouse, 18/06/14 – 20/06/14, Springer, LNCS 8535, juin 2014.
Résumé Accès : www.springer.com
BibTeXYamine Ait Ameur, Witold Andrzejewski, Ladjel Bellatreche, Barbara Catania, Tania Cerquitelli, Silvia Chiusano, Matteo Golfarelli, Giovanna Guerrini, Krzystof Kaczmarski, Mirko Kampf, Alfons Kemper, Tobias Lauer, Boris Novikov, Themis Palpanas, Jaroslav Pokorny, Stefano Rizzi, Athena Vakali
New Trends in Databases and Information Systems: Contributions from ADBIS 2013, Genoa, Italie, 01/09/13 – 04/09/13, Springer, AISC : Advances in Intelligent Systems and Computing 241 ISBN 978-3-319-01862-1, septembre 2013.
Résumé Accès : https://doi.org/10.1007/978-3-319-01863-8_1
BibTeXIdir Ait-Sadoune, Yamine Ait Ameur
Stepwise Development of Formal Models for Web Services Compositions: Modelling and Property Verification, Vienne, Autriche, 02/09/14 – 06/09/14, Springer-Verlag, LNCS 7446, septembre 2012.
Sébastien Maitrehenry, Sylvain Metge, Yamine Ait Ameur, Pierre Bieber
MEDI, Poitiers, France, 03/10/14 – 05/10/14, Springer-Verlag, LNCS 7602, octobre 2012.
Yamine Ait Ameur, Dominique Méry
ISOLA, Heraklion – Grèce, 15/10/12 – 18/10/12, Springer-Verlag, LNCS 7610, octobre 2012.
Rigorous Safety-Critical Cyber-Physical Systems Development using Formal Methods
Computer Science [cs]. Toulouse INP, 2024
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⟩
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⟩
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 : ⟩
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⟩
Algorithms and techniques for bot detection in social networks
Library and information sciences. Université Paul Sabatier – Toulouse III; ITMO University, 2021. English. ⟨NNT : 2021TOU30097⟩
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⟩
On the Power of Rounds: Explorations of the Heard-Of Model
Distributed, Parallel, and Cluster Computing [cs.DC]. Université de Toulouse, 2020. English. ⟨NNT : ⟩
A formal framework for heterogeneous systems semantics
Networking and Internet Architecture [cs.NI]. Institut National Polytechnique de Toulouse – INPT, 2020. English. ⟨NNT : 2020INPT0072⟩
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⟩
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
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
Xavier Thirioux, Alexis Maffart
Taylor Series Revisited
ISAE/DISC/RT2020/1, Institut Supérieur de l’Aéronautique et de l’Espace. 2020
Érik Martin-Dorel, Sergei Soloviev
A Formal Study of Boolean Games with Random Formulas as Pay Functions
[Research Report] IRIT. 2017
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker
Rapport de recherche, 0, Archive of Formal Proofs, septembre 2016.
Accès : https://www.isa-afp.org/entries/CAVA_LTL_Modelchecker.shtml
BibTeXZhibin Yang, Jean-Paul Bodeveix, Mamoun Filali
Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties
Rapport de recherche, IRIT/RT–2014-02–FR, IRIT, décembre 2014.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions in Coq
Rapport de recherche, IRIT/RR–2014-09–FR, IRIT, novembre 2014.
Accès : http://www.irit.fr/publis/ACADIE/IRIT-RR-2014-09-FR.pdf
BibTeXManuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Concurrent Systems with Priorities
Rapport de recherche, Report–2013-16–FR, IRIT, juin 2013.
Résumé Accès : http://www.irit.fr/~Manuel.Garnacho/Publications/MechPrio.pdf
BibTeXManuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Concurrent Systems with Priorities
Rapport de recherche, RIT/RR–2013-16–FR, IRIT, février 2013.
Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Real-Time Concurrent Systems
Rapport de recherche, IRIT/RR–2013-15–FR, IRIT, janvier 2013.
Univariate and Bivariate Integral Roots Certificates Based on Hensel’s Lifting
Rapport de recherche, RRLIP2011-1, LIP, Ecole Normale Supérieure de Lyon, mars 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Verification of Timed BPEL 2.0 Models
Rapport de recherche, IRIT/RR2011-10FR, IRIT, mars 2011.
Jacques Cazin, Pierre-Loïc Garoche, Marc Pantel, Virginie Wiels
D2.5.1 ES_PASS qualification guidelines for static analysis based verification tools
Rapport de contrat, D2.5.1, Institut National Polytechnique de Toulouse, novembre 2009.
Vérification de transformations de modèles
Rapport de Master, IRIT, juin 2009.
Résumé Accès : http://www.irit.fr/publis/ACADIE/M2RRapport.pdf
BibTeX
contrats de l’équipe
Acronyme | Titre | Resp. sc | Début-Fin | |
---|---|---|---|---|
EBRP-EventB-Rodin-Plus | Enrichissement de EventB et de RODIN | Yamine AIT AMEUR | 2020 – 2026 | |
Learn OCaml 2022-2026 | Convention de financement pour l’accueil d’étudiants stagiaires LearnOCaml 2022-2026 | Erik MARTIN-DOREL | 2022 – 2026 | |
ProTiPP | Proved Timing-Predictable Processors | Christine ROCHANGE | 2023 – 2027 | |
ForML – Toulouse INP | Formally Certified Reasoning in Machine Learning – Partie Toulouse INP | André-Luc BEYLOT Aurélie HURAULT | 2024 – 2027 | |
Learn OCaml 2021 [Contrat terminé] | Learn OCaml 2021 | Erik MARTIN-DOREL | 2021 – 2021 | |
ICSPA [Contrat terminé] | Assistants de preuve basés sur la théorie des ensembles interopéables et sûres | Yamine AIT AMEUR | 2020 – 2024 | |
Learn OCaml 2020 [Contrat terminé] | Learn OCaml 2020 | Erik MARTIN-DOREL | 2020 – 2020 | |
Learn OCaml 2019 [Contrat terminé] | Learn OCaml 2019 | Erik MARTIN-DOREL | 2019 – 2019 | |
DISCONT [Contrat terminé] | Intégration correcte de modèles discrets et continus | Neeraj SINGH | 2017 – 2022 | |
Slevogt [Contrat terminé] | Financement de la préparation du projet SLEVOGT | Martin STRECKER | 2017 – 2017 | |
FORMEDICIS [Contrat terminé] | Méthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques | Yamine AIT AMEUR | 2016 – 2021 | |
PARDI [Contrat terminé] | Vérification de systèmes distribués paramétrés | Philippe QUÉINNEC | 2016 – 2021 | |
2017-013 [Contrat terminé] | Ingénierie formelle des systèmes embarqués | Marc PANTEL | 2016 – 2018 | |
AMANDE [Contrat terminé] | Advanced Multilateral Argumentation for Deliberation | | 2013 – 2017 | |
BRIEFCASE [Contrat terminé] | Convention de soutien à un projet rattaché à un chantier : N°RTRA-STAE/2011/BRIEFCASE/06 | Marc PANTEL | 2013 – 2014 | |
IMPEX [Contrat terminé] | Integration des semantique implicite et explicite dans le développement de systèmes discrets fondés sur la panne | Yamine AIT AMEUR | 2013 – 2017 | |
PANDA [Contrat terminé] | Plateforme avionique modulaire etendue | Yamine AIT AMEUR | 2013 – 2015 | |
VORACE [Contrat terminé] | Vérification des optimisations rapides appliquées à la commande embarquée | Marc PANTEL | 2013 – 2016 |
Acronyme | Titre | Resp. sc | Début-Fin |
---|
Acronyme | Titre | Resp. sc | Début-Fin |
---|