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
Members team
- Yamine AIT AMEURProfessor – Toulouse INP
- Jean-Paul BODEVEIXProfessor – UT3
- Christelle CHAUDETAssociate Professor – UT3
- Xavier CRÉGUTAssociate Professor – Toulouse INP
- Guillaume DUPONTAssociate Professor – Toulouse INP
- Mamoun FILALIResearch Scientist – CNRS
- Aurélie HURAULTAssociate Professor (HDR) – Toulouse INP
- Erik MARTIN-DORELAssociate Professor – UT3
- Ralph MATTHESResearch Scientist (HDR) – CNRS
- Philippe MAURANAssociate Professor – Toulouse INP
- Meriem OUEDERNIAssociate Professor – Toulouse INP
- Marc PANTELAssociate Professor – Toulouse INP
- Philippe QUÉINNECProfessor – Toulouse INP
- Jean-Baptiste RACLETAssociate Professor – UT3
- Neeraj SINGHAssociate Professor – Toulouse INP
- Jan-Georg SMAUSProfessor – UT3
- Sergei SOLOVIEVProfessor – UT3
- Martin STRECKERAssociate Professor – UT3
- Yannis BENABBIPhD Student – Toulouse INP
- Amine BENCHAABOUNIntern M1 – Toulouse INP
- Benjamin CHAMAYOUIntern L – Toulouse INP
- Clément CONTETIntern – Toulouse INP
- Hugo DELEYEIntern M1 – ANITI
- Romain DORÉIntern M1 – UT3 (joint direction TALENT)
- Alexandre DUBOISTeacher-researcher MAST – UT3
- Issam EL KHARRAZIntern M1 – Toulouse INP
- Gregoire HONVAULTIntern M1 – Toulouse INP
- Zhao JINIntern M1 – UT3
- Dominique KITCHIGUINIntern L – UT3
- Mael MATHURINIntern M1 – Toulouse INP
- Ismail MENDILPhD Student – Toulouse INP
- Pierre POMERET-COQUOTPhD Student – UT3 (joint direction ADRIA)
- Mika PONSPhD Student – UT Capitole (joint direction SMART, TALENT)
- Peter RIVIEREPhD Student – Toulouse INP
- Louis TARIOTIntern M1 – ISAE SUPAERO
- Guillaume VERDIERResearch Engineer – Autre tutelle
- Elie FARESAssociate teacher-researcher – Ras al Khaimah – UAE
- Raju HALDERTeacher-researcher Invité – DEPARTEMENT OF COMPUTER
- Ferhat KHENDEKTeacher-researcher Invité – Université de concordia
- Benoit MORGANAssociate teacher-researcher – Autre
- Klaus-Dieter SCHEWETeacher-researcher Invité – UNIVERSITE DE
- Xavier THIRIOUXTeacher-researcher – ISAE
publications team
Frédéric Boniol, Virginie Wiels, Yamine Ait Ameur, Klaus-Dieter Schewe
The landing gear case study: challenges and experiments
In : International Journal on Software Tools for Technology Transfer, Springer-Verlag, Heidelberg, Allemagne, Vol. 19 N. 2, pp. 133-140, 2016.
Yamine Ait Ameur, Dominique Méry
Making explicit domain knowledge in formal system development
In : Science of Computer Programming, Elsevier, Vol. 121, pp. 100-127, 2016.
Mounira Kezadri, Marc Pantel, Xavier Thirioux, Benoit Combemale
Correct-by-construction model driven engineering composition operators
In : Formal Aspects of Computing, Springer, Vol. 28 N. 3, pp. 409-440, 2016.
Florent Chevrou, Aurélie Hurault, Philippe Quéinnec
On the Diversity of Asynchronous Communication
In : Formal Aspects of Computing, Springer, Vol. 28 N. 5, pp. 847-879, September 2016.
URL : 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
In : Optimization Engineering, Taylor & Francis Group, Vol. 17 N. 4, pp. 781-812, December 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
In : International Journal of Intelligent Systems Technologies and Applications, Inderscience Publishers, Vol. 15 N. 2, pp. 95-126, 2016.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
In : Journal of Automated Reasoning, Springer-Verlag, Heidelberg, Allemagne, Vol. 57 N. 3, pp. 187-217, October 2016.
Abstract URL : 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
In : International Journal of Semantic Computing, World Scientific, Vol. 9 N. 1, pp. 105-138, 2015.
URL : 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.
In : Computing, Springer, Vol. 7 N. 97, pp. 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
In : Journal of Advanced Computational Intelligence, Fuji Technology Press, Tokyo, Vol. 19 N. 5, pp. 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
In : Frontiers of Computer Science, Springer, Vol. 10, N. 1, pp. 37-53, February 2016.
Zhibin Yang, Kai Hu, Yongwang Zhao, Dianfu Ma, Jean-Paul Bodeveix
AADL Model Verification by Translating into TASM
In : Journal of Software, Institute of Software Chinese Academy of Science (ISCAS), China, Vol. 26, N. 2, pp. 1-20, February 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
In : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Special issue La composition d’objets, de composants et de services, Vol. 30, N. 6/2011, pp. 685-710, June 2011.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
Expérimentations en Coq pour un générateur de code qualifiable
In : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Special issue Méthodes formelles à l’analyse et la compilation, Vol. 30, N. 4/2011, pp. 409-440, April 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
In : Journal of Software, Institute of Software Chinese Academy of Science (ISCAS), China, Vol. 21, N. 5, pp. 899-915, May 2010.
URL : 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
In : 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, pp. 31-37, February 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
In : L’Objet, Hermès Science, Special issue Composants, services et aspects techniques et outils pour la vérification, Vol. 14, N. 4, pp. 43-72, December 2008.
Olga Antonova, Sergei Soloviev
Le test de Turing et la question d’une definition de la realite virtuelle
In : Logiko-philosophskie shtudii. (Etudes logiko-philosophiques), Universite d’Etat de St. Petersbourg, Russia, Vol. 5, pp. 50-67, 2008.
Benoit Combemale, Xavier Crégut, Pierre Michel, Marc Pantel
SéMo’07 : premier atelier sur la Sémantique des Modèles
In : L’Objet, Hermès Science, Special issue Ingénierie Dirigée par les Modèles, Vol. 13, N. 4, pp. 137-144, January 2008.
Olga Antonova, Sergei Soloviev
Axiomatika i ochevidnost. (Axiomatique et evidence.)Logiko-philosophskie shtudii, 4, Universite d’Etat de St. Petersbourg
In : Logiko-philosophskie shtudii. (Etudes logiko-philosophiques), Universite d’Etat de St. Petersbourg, Russia, Vol. 4, pp. 3-11, August 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.
URL : 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.
Sarah Benyagoub, Meriem Ouederni, Yamine Ait Ameur
Towards correct Evolution of Conversation Protocols (regular paper)
In : International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2016), Tunis, Tunisie, 06/10/16-07/10/16, Vol. 1689, Mohamed GHAZEL, Mohamed JMAIEL (Eds.), CEUR-WS : Workshop proceedings, pp. 193-201, October 2016.
Abstract URL : http://ceur-ws.org/Vol-1689/paper16.pdf – https://oatao.univ-toulouse.fr/24899/
BibTeXSarah Benyagoub, Meriem Ouederni, Neeraj Singh, Yamine Ait Ameur
Correct-by-Construction Evolution of Realisable Conversation Protocols (regular paper)
In : Model and Data Engineering International Conference (MEDI 2016), Almeria, Espagne, 21/09/16-23/09/16, Vol. 9893, Ladjel BELLATRECHE, Oscar PASTOR, Jesus Manuel ALMENDROS-JIMENEZ, Yamine AIT AMEUR (Eds.), Springer-Verlag, LNCS ISBN 978-3-319-45546-4, pp. 260-273, September 2016.
Abstract URL : https://doi.org/10.1007/978-3-319-45547-1_21 – https://oatao.univ-toulouse.fr/24898/
BibTeXKahina Hacid, Yamine Ait Ameur
Annotation of Engineering Models by References to Domain Ontologies (regular paper)
In : Model and Data Engineering International Conference (MEDI 2016), Almeria, Espagne, 21/09/16-23/09/16, Vol. 9893, Ladjel BELLATRECHE, Oscar PASTOR, Jesus Manuel ALMENDROS-JIMENEZ, Yamine AIT AMEUR (Eds.), Springer-Verlag, LNCS ISBN 978-3-319-45546-4, pp. 234-244, September 2016.
Abstract URL : https://doi.org/10.1007/978-3-319-45547-1_19 – https://oatao.univ-toulouse.fr/24897/
BibTeXKahina Hacid, Yamine Ait Ameur
Strengthening MDE and Formal Design Models by References to Domain Ontologies. A Model Annotation Based Approach (regular paper)
In : International on Symposium Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Corfu, Grèce, 10/10/16-14/10/16, Vol. 9952, Tiziana MARGARIA, Bernhard STEFFEN (Eds.), Springer-Verlag, LNCS ISBN 978-3-319-47165-5, pp. 340-357, October 2016.
Abstract URL : https://doi.org/10.1007/978-3-319-47166-2_24 – https://oatao.univ-toulouse.fr/24896/
BibTeXJon Haël Brenas, Rachid Echahed, Martin Strecker
Ensuring Correctness of Model Transformations While Remaining Decidable (regular paper)
In : International Colloquium on Theoretical Aspects of Computing (ICTAC 2016), Taipei, Taiwan, ROC, 24/10/16-31/10/16, Vol. 9965, Augusto Sampaio, Farn Wang (Eds.), Springer, Lecture Notes in Computer Science, pp. 315-332, October 2016.
Abstract URL : https://doi.org/10.1007/978-3-319-46750-4_18
BibTeXJon Haël Brenas, Rachid Echahed, Martin Strecker
Proving Correctness of Logically Decorated Graph Rewriting Systems (regular paper)
In : International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal, 22/06/16-26/06/16, Delia Kesner, Brigitte Pientka (Eds.), Schloss Dagstuhl Leibniz-Zentrum fur Informatik, (on line), June 2016.
Abstract URL : https://doi.org/10.4230/LIPIcs.FSCD.2016.14 – https://oatao.univ-toulouse.fr/22715/
BibTeXJon Haël Brenas, Rachid Echahed, Martin Strecker
On the Closure of Description Logics under Substitutions (regular paper)
In : International Workshop on Description Logics (DL workshop 2016), Cape Town, South Africa, 22/04/16-25/04/16, Vol. 1577, Maurizio Lenzerini, Rafael Penaloza (Eds.), CEUR-WS : Workshop proceedings, (on line), April 2016.
Abstract URL : http://ceur-ws.org/Vol-1577/paper_47.pdf – https://oatao.univ-toulouse.fr/22714/
BibTeXPierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
Hierarchical State Machines as Modular Horn Clauses (regular paper)
In : Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016), Eindhoven, The Netherlands, 03/04/16, Vol. 219, Electronic Proceedings in Theorical Computer Science (EPTCS), pp. 15-28, April 2016.
Abstract URL : https://doi.org/10.4204/EPTCS.219.2 – https://oatao.univ-toulouse.fr/22653/
BibTeXNeeraj Singh, Yamine Ait Ameur, Marc Pantel, Arnaud Dieumegard, Eric Jenn
Stepwise Formal Modeling and Verification of Self-Adaptive Systems with Event-B. The Automatic Rover Protection Case Study (regular paper)
In : IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2016), Dubaï, Emirats Arabes Unis, 06/11/16-08/11/16, IEEE Computer Society, pp. 43-52, November 2016.
Faiez Zalila, Xavier Crégut, Marc Pantel
A DSL to Feedback Formal Verification Results (regular paper)
In : Model-Driven Engineering, Verification and Validation Workshop at the MODELS conference (MODEVVA 2016), Saint Malo, France, 03/10/16, Vol. 1713, CEUR-WS : Workshop proceedings, pp. 30-39, October 2016.
URL : http://ceur-ws.org/Vol-1713/MoDeVVa_2016_paper_4.pdf
BibTeX
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, Mamoun Filali
An Event-B development process for the distributed BIP framework
In : FAC, Toulouse, 30/03/16-31/03/16.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
In : Journées FAC 2016, LAAS, Toulouse, 30/03/16-31/03/16.
URL : 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
In : The MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, CIRM, Luminy, Marseille, 11/01/16-15/01/16.
Formal proofs and certified computation in Coq
In : 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
In : 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
In : 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
In : CONAIS 2012 (9o Congreso Nacional y 6o Internacional de Informática y Sistemas), Villahermosa (Mexique), 19/09/12-21/09/12 (invited speaker).
Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann
Implementations of two algorithms for the threshold synthesis problem
In : International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, 09/01/12-11/01/12 (invited speaker).
Abstract URL : http://www.cs.uic.edu/pub/Isaim2012/WebPreferences/ISAIM2012_Boolean_Schilling_etal.pdf
BibTeXUnivariate and Bivariate Integral Roots Certificates Based on Hensel Lifting
In : The Third Coq Workshop 2011, Nijmegen, Netherlands, 26/08/11-26/08/11, Bas Spitters (Eds.).
URL : http://www.cs.ru.nl/~spitters/coqw_files/program.html
BibTeXElie Fares, Jean-Paul Bodeveix, Mamoun Filali
A Transformation and Verification Framework for BPEL
In : 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, and Shahnaz Fatima. Distributed Computing to Blockchain: Architecture, Technology, and Applications, pp.332, In press, 978-0323961462
Yamine Aït-Ameur, Guillaume Dupont, Ismail Mendil, Dominique Méry, Marc Pantel, Peter Rivière, Neeraj Singh
Empowering the Event-B Method Using External Theories
Integrated Formal Methods, 13274, Springer International Publishing, pp.18-35, 2022, Lecture Notes in Computer Science, 978-3-031-07726-5. ⟨10.1007/978-3-031-07727-2_2⟩
Jonathan Certes, Benoît Morgan
Remote attestation of bare-metal microprocessor software: a formally verified security monitor
Database and Expert Systems Applications – DEXA 2021 Workshops: BIOKDD, IWCFS, MLKgraphs, AI-CARES, ProTime, AISys 2021, Virtual Event, September 27–30, 2021, Proceedings, 1479, Springer International Publishing, pp.42-51, 2021, Communications in Computer and Information Science book series (CCIS), 978-3-030-87100-0. ⟨10.1007/978-3-030-87101-7_5⟩
José Espírito Santo, Ralph Matthes, Luís Pinto
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
Ugo de’Liguoro; Stefano Berardi; Thorsten Altenkirch. LIPIcs : 26th International Conference on Types for Proofs and Programs (TYPES 2020), 188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany, 2021, LIPIcs : Leibniz International Proceedings in Informatics ; ISSN : 1868-8969, 978-3-95977-182-5. ⟨10.4230/LIPIcs.TYPES.2020.4⟩
Yamine Aït-Ameur, Régine Laleau, Dominique Méry, Neeraj Kumar Singh
Towards Leveraging Domain Knowledge in State-Based Formal Methods
Raschke, Alexander; Riccobene, Elvinia; Schewe, Klaus-Dieter. Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday, 12750, Springer, pp.1-13, 2021, Lecture Notes in Computer Science, 978-3-030-76020-5. ⟨10.1007/978-3-030-76020-5_1⟩
Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry
Formal Ontological Analysis for Medical Protocols
Implicit and explicit semantics integration in proof based developments of discrete systems, Springer, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6_5⟩
Yamine Aït-Ameur, Shin Nakajima, Dominique Méry
Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems
Springer Singapore, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6⟩
Ulrich Berger, Ralph Matthes, Anton Setzer
Martin Hofmann’s Case for Non-Strictly Positive Data Types
Peter Dybjer; José Espírito Santo; Luís Pinto. 24th International Conference on Types for Proofs and Programs (TYPES 2018), 130, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp.1:1-1:22, 2019, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-106-1. ⟨10.4230/LIPIcs.TYPES.2018.1⟩
Benedikt Ahrens, Ralph Matthes
Heterogeneous Substitution Systems Revisited
Tarmo Uustalu. 21st International Conference on Types for Proofs and Programs (TYPES 2015), 69, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp.2:1-2:23, 2018, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-030-9. ⟨10.4230/LIPIcs.TYPES.2015.2⟩
Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Albert Sangiovanni-Vincentelli, Werner Damm, Thomas Henzinger, Kim G. Larsen
Contracts for System Design
Now Publishers, 12 (2-3), pp.124-400, 2018, Foundations and Trends® in Electronic Design Automation, 978-1-68083-402-4. ⟨10.1561/1000000053⟩
Verifying Embedded Systems
HDR, Institut National Polytechnique de Toulouse, September 2016.
Systematic use of models of concurrency in executable domain-specific modelling languages
Master’s Thesis, Institut National Polytechnique de Toulouse, July 2016.
Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes
Master’s Thesis, Université de Toulouse, March 2016.
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.
Formal Guaranties for Safety Critical Code Generation : the Case of Highly Variable Languages
Master’s Thesis, Institut National Polytechnique de Toulouse, January 2015.
Methods and tools for the integration of formal verification in domain-specific languages
Master’s Thesis, Institut National Polytechnique de Toulouse, December 2014.
Investigation dans des systèmes abstraits avec entrées et sorties comme fonctions partielles de temps
Master’s Thesis, Université Paul Sabatier, December 2014.
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
BibTeXApproche ADL pour la modélisation d’architecture basée sur les contraintes (calcul de WCET)
Master’s Thesis, Université Paul Sabatier, September 2014.
Property Driven Verification Framework: Application to Real-Time Property for UML-MARTE Software Designs
Master’s Thesis, Institut National Polytechnique de Toulouse, May 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
Research report, 0, Archive of Formal Proofs, September 2016.
URL : 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
Research report, IRIT/RT–2014-02–FR, IRIT, December 2014.
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions in Coq
Research report, IRIT/RR–2014-09–FR, IRIT, November 2014.
URL : 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
Research report, Report–2013-16–FR, IRIT, June 2013.
Abstract URL : http://www.irit.fr/~Manuel.Garnacho/Publications/MechPrio.pdf
BibTeXManuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Concurrent Systems with Priorities
Research report, RIT/RR–2013-16–FR, IRIT, February 2013.
Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
Mechanized Semantics of Real-Time Concurrent Systems
Research report, IRIT/RR–2013-15–FR, IRIT, January 2013.
Univariate and Bivariate Integral Roots Certificates Based on Hensel’s Lifting
Research report, RRLIP2011-1, LIP, Ecole Normale Supérieure de Lyon, March 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Verification of Timed BPEL 2.0 Models
Research report, IRIT/RR2011-10FR, IRIT, March 2011.
Jacques Cazin, Pierre-Loïc Garoche, Marc Pantel, Virginie Wiels
D2.5.1 ES_PASS qualification guidelines for static analysis based verification tools
Contract report, D2.5.1, Institut National Polytechnique de Toulouse, November 2009.
Vérification de transformations de modèles
Master’s report, IRIT, June 2009.
Abstract URL : http://www.irit.fr/publis/ACADIE/M2RRapport.pdf
BibTeX
Contracts team
| 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 [Contract completed] | | 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] | | 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 [Contract completed] | | Intégration correcte de modèles discrets et continus | Neeraj SINGH | 2017 – 2022 |
| Slevogt [Contract completed] | Financement de la préparation du projet SLEVOGT | Martin STRECKER | 2017 – 2017 | |
| FORMEDICIS [Contract completed] | Méthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques | Yamine AIT AMEUR | 2016 – 2021 | |
| PARDI [Contract completed] | Vérification de systèmes distribués paramétrés | Philippe QUÉINNEC | 2016 – 2021 | |
| AMANDE [Contract completed] | Advanced Multilateral Argumentation for Deliberation | Xavier THIRIOUX | 2013 – 2017 | |
| BRIEFCASE [Contract completed] | Convention de soutien à un projet rattaché à un chantier : N°RTRA-STAE/2011/BRIEFCASE/06 | Marc PANTEL | 2013 – 2014 | |
| 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 | |
| PANDA [Contract completed] | Plateforme avionique modulaire etendue | Yamine AIT AMEUR | 2013 – 2015 | |
| VORACE [Contract completed] | Vérification des optimisations rapides appliquées à la commande embarquée | Marc PANTEL | 2013 – 2016 |
| Acronyme | Titre | Resp. sc | Début – fin |
|---|