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
- Mamoun FILALIChargé de Recherche – CNRS
- Aurélie HURAULTMaître de Conférences (HDR) – Toulouse INP
- Erik MARTIN-DORELMaître de Conférences – UT3
- Ralph MATTHESChargé de Recherche (HDR) – CNRS
- Philippe MAURANMaître de Conférences – Toulouse INP
- Meriem OUEDERNIMaître de Conférences – Toulouse INP
- Marc PANTELMaître de Conférences – Toulouse INP
- Philippe QUÉINNECProfesseur – Toulouse INP
- Jean-Baptiste RACLETMaître de Conférences – UT3
- Neeraj SINGHMaître de Conférences – Toulouse INP
- Jan-Georg SMAUSProfesseur – UT3
- Sergei SOLOVIEVProfesseur – UT3
- Martin STRECKERMaître de Conférences – UT3
- Yannis BENABBIDoctorant – Toulouse INP
- Alexandre DUBOISEnseignant-chercheur MAST – UT3
- Anne GRIEUDoctorant – Toulouse INP
- Ismail MENDILDoctorant – Toulouse INP
- Pierre POMERET-COQUOTDoctorant – UT3 (co-encadrement ADRIA)
- Mika PONSDoctorant – UT Capitole (co-encadrement SMART, TALENT)
- Peter RIVIEREDoctorant – Toulouse INP
- Guillaume VERDIERIngénieur de Recherche – Autre tutelle
- Elie FARESEnseignant-chercheur Associé – Ras al Khaimah – UAE
- Benoit MORGANEnseignant-chercheur Associé – Autre
- Xavier THIRIOUXEnseignant-chercheur – ISAE
publications de l’équipe
Frédéric Boniol, Virginie Wiels, Yamine Ait Ameur, Klaus-Dieter Schewe
The landing gear case study: challenges and experiments
Dans : International Journal on Software Tools for Technology Transfer, Springer-Verlag, Heidelberg, Allemagne, Vol. 19 N. 2, p. 133-140, 2016.
Yamine Ait Ameur, Dominique Méry
Making explicit domain knowledge in formal system development
Dans : Science of Computer Programming, Elsevier, Vol. 121, p. 100-127, 2016.
Mounira Kezadri, Marc Pantel, Xavier Thirioux, Benoit Combemale
Correct-by-construction model driven engineering composition operators
Dans : Formal Aspects of Computing, Springer, Vol. 28 N. 3, p. 409-440, 2016.
Florent Chevrou, Aurélie Hurault, Philippe Quéinnec
On the Diversity of Asynchronous Communication
Dans : Formal Aspects of Computing, Springer, Vol. 28 N. 5, p. 847-879, septembre 2016.
Accès : http://queinnec.perso.enseeiht.fr/publis/Formaspects.pdf – https://oatao.univ-toulouse.fr/16963/
BibTeXTimothy Wang, Romain Jobredeaux, Marc Pantel, Pierre-Loïc Garoche, Eric Feron, Didier Henrion
Credible Autocoding of Convex Optimization Algorithms
Dans : Optimization Engineering, Taylor & Francis Group, Vol. 17 N. 4, p. 781-812, décembre 2016.
Serial Rayene Boussalia, Allaoua Chaoui, Aurélie Hurault, Meriem Ouederni, Philippe Quéinnec
Multi-objective quantum inspired Cuckoo search algorithm and multi-objective bat inspired algorithm for the web service composition problem
Dans : International Journal of Intelligent Systems Technologies and Applications, Inderscience Publishers, Vol. 15 N. 2, p. 95-126, 2016.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
Dans : Journal of Automated Reasoning, Springer-Verlag, Heidelberg, Allemagne, Vol. 57 N. 3, p. 187-217, octobre 2016.
Résumé Accès : http://dx.doi.org/10.1007/s10817-015-9350-4 – http://www.irit.fr/publis/ACADIE/CoqInterval-JAR.pdf – https://oatao.univ-toulouse.fr/16862/
BibTeXStéphane Jean, Yamine Ait Ameur, Guy Pierra
OntoQL: An Alternative to Semantic Web Query Languages
Dans : International Journal of Semantic Computing, World Scientific, Vol. 9 N. 1, p. 105-138, 2015.
Accès : https://doi.org/10.1142/S1793351X1550004X – https://oatao.univ-toulouse.fr/24849/
BibTeXLinda Mohand Oussaid, Yamine Ait Ameur, Idir Ait Sadoune, Mohamed Ahmed Nacer
A formal model for output multimodal HCI – An Event-B formalization.
Dans : Computing, Springer, Vol. 7 N. 97, p. 713-740, 2015.
Joe Lorkowski, Olga Kosheleva, Vladik Kreinovich, Sergei Soloviev
How Design Quality Improves with Increasing Computational Abilities: General Formulas and Case Study of Aircraft Fuel Efficiency
Dans : Journal of Advanced Computational Intelligence, Fuji Technology Press, Tokyo, Vol. 19 N. 5, p. 581-584, 2015.
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.
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.
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⟩
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⟩
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
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
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), https://www.erts2022.org/, 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⟩
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
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.
Abdeldjalil Boudjadar, Jean-Paul Bodeveix, Mamoun Filali
Revising and Extending the Uppaal Communication Mechanism, Springer-Verlag, Vol. 7306, Lecture Notes in Computer Science, juin 2012.
Olga Antonova, Sergei Soloviev
La théorie et la pratique de la réalité virtuelle: l’analyse logique et philosophique., Universite d’Etat de St. Petersbourg, août 2008.
J.-M. Farines, Bernard Berthomieu, Jean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, Hicham Hafidi, Jean-Luc Lambert, Pierre Michel, François Vernadat
The Cotre Project: Rigorous Software Development for Real Time Systems in Avionics, COLNARIC, ADAMSKI & WEGRZYN, novembre 2003.
Jean-Paul Bodeveix, Mamoun Filali, Amal Sayah
Programmation en C++, InterEditions, 1994.
Pierre Dissaux, Mamoun Filali, Pierre Michel, François Vernadat
Architecture Description languages
, Springer, avril 2005.
Jean-Paul Bodeveix, Thierry Millan, Christian Percebois, Pierre Bazex, Louis Féraud
NEPTUNE : Method, Checking and documentation generation for UML application
, NEPTUNE Consortium, 2003.
Guillaume Babin, Yamine Ait Ameur, Marc Pantel
A generic model for system substitution
Dans : Trustworthy Cyber-Physical Systems Engineering. Alexander Romanovsky, Fuyuki Ishikawa (Eds.) , Chapman & Hall, CRC Press, 4, p. 75-103, Computer and Information Science Series, septembre 2016.
Accès : https://www.crcpress.com/Trustworthy-Cyber-Physical-Systems-Engineering/Romanovsky-Ishikawa/9781498742450
BibTeXTimothy Wang, Romain Jobredeaux, Heber Henrencia, Pierre-Loïc Garoche, Eric Feron, Marc Pantel
From Design to Implementation: An Automated Credible Autocoding Chain for Control Systems
Dans : Advances in Control System Technology for Aerospace Applications. Eric Féron (Eds.) , Springer-Verlag, p. 137-180, 2016.
Idir Ait Sadoune, Yamine Ait Ameur
Formal Modelling and Verification of Transactional Web Service Composition: A Refinement and Proof Approach with Event-B.
Dans : Correct Software in Web Applications and Web Services. Bernhard THALHEIM, Klaus-Dieter SCHEWE, Andreas PRINZ, Bruno BUCHBERGER (Eds.) , Springer, p. 1-27, ISBN 978-3-319-17111-1, 2015.
The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics
Dans : 19th International Conference on Types for Proofs and Programs (TYPES 2013). Ralph Matthes, Aleksy Schubert (Eds.) , Dagstuhl Publishing, p. 202-229, Vol. 26, Leibniz International Proceedings in Informatics (LIPIcs), 2014.
Résumé Accès : http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.202
BibTeX
Verifying Embedded Systems
Habilitation à diriger des recherches, Institut National Polytechnique de Toulouse, septembre 2016.
Systematic use of models of concurrency in executable domain-specific modelling languages
Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2016.
Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes
Thèse de doctorat, Université de Toulouse, mars 2016.
Une théorie mécanisée des arbres réguliers en théorie des types dépendants
Thèse de doctorat, Université Paul Sabatier, mai 2016.
Formal Guaranties for Safety Critical Code Generation : the Case of Highly Variable Languages
Thèse de doctorat, Institut National Polytechnique de Toulouse, janvier 2015.
Methods and tools for the integration of formal verification in domain-specific languages
Thèse de doctorat, Institut National Polytechnique de Toulouse, décembre 2014.
Investigation dans des systèmes abstraits avec entrées et sorties comme fonctions partielles de temps
Thèse de doctorat, Université Paul Sabatier, décembre 2014.
Analyse formellement vérifiée des conflits de partage de ressources en Java multi-tâche
Thèse de doctorat, Université Paul Sabatier, décembre 2014.
Résumé Accès : http://www.irit.fr/publis/ACADIE/main.pdf
BibTeXApproche ADL pour la modélisation d’architecture basée sur les contraintes (calcul de WCET)
Thèse de doctorat, Université Paul Sabatier, septembre 2014.
Property Driven Verification Framework: Application to Real-Time Property for UML-MARTE Software Designs
Thèse de doctorat, Institut National Polytechnique de Toulouse, mai 2014.
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
É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 – 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 | |
| CLIMT [Contrat terminé] | | Méthodes catégoriques et logiques en transformations de modèles | Ralph MATTHES | 2012 – 2016 |
| GeMoC [Contrat terminé] | 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 [Contrat terminé] | | Vérification formelle d’un générateur de code pour un langage synchrone | Martin STRECKER | 2010 – 2014 |
| Acronyme | Titre | Resp. sc | Début – fin | |
|---|---|---|---|---|
| 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 | |
| AMANDE [Contrat terminé] | Advanced Multilateral Argumentation for Deliberation | Xavier THIRIOUX | 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 |
|---|