Research

Current research interests

Correctness of program and component software properties obtained by construction via language design or derivation from specifications, or obtained by a posteriori verification, in particular collaborative verification including deductive verification. Applied formal methods in the context of security and the internet of things.

Research results are presented in my papers and talks (sorted by year, in DBLP).

Postdoctoral Researchers and Research Engineers

• Myriam Clouet, LIFO, Orléans

Students

• PhD students:
  • Téo Bernier (supervised with N. Kosmatov), LIFO, Orléans
  • Jérémy Damour (supervised with L. Correnson, A. Blanchard), CEA List and LIFO
  • Florian Groult (supervised with F. Dabrowski), LIFO, Orléans
  • Jordan Ischard (supervised with J. Chouquet), LIFO, Orléans
  • Yani Ziani (supervised with N. Kosmatov), Thales Research & Technology and LIFO

Ongoing projects

Funded Projects

• 2025-2028: For-CoaLa Formalization of Configuration Languages (355k€ incl. 165k€ for LIFO, funded by Agence Nationale de la Recherche, ANR). PI: Hélène Coullon. Role: co-PI. Partners: IMT Atlantique; LIFO, Université d'Orléans.
• 2025-2026: VéDySec Vérification Dynamique pour la Sécurité (424k€ incl. 72k€ for LIFO, funded by Agence de l'Innovation de Défense, AID). PI: Nikolai Kosmatov. Role: co-PI. Partners: Université d'Orléans, LIFO; CEA List; Thales Research & Technology.
• 2023-2026: CoMeMoV Collaborative Memory Models for formal Verification (514k€, funded by Agence Nationale de la Recherche, ANR). Role: PI. Partners: Université d'Orléans, LIFO; CEA List; Thales Research & Technology.
• 2024-2025: ACCEPTALGO (112k€, funded by Région Centre Val de Loire. PI: Beatrice Boulu-Reshef. Role: co-PI)
• 2023-2024: SIOMediC ― Sécurité de l’Internet des Objets Médicaux Connectés / Security of the Internet of Medical Things (99k€, funded by Région Centre Val de Loire. PI: Patrice Clemente. Role: co-PI)

Software Projects

• From 2023: Functional Bulk Synchronous Parallel Programming with Why3 (WhyBSML)
• From 2017: Frama-C for the Internet of Things (Frama-C for IoT)
• From 2009: Systematic Development of Programs for Parallel and Cloud Computing (SyDPaCC)
• From 1998: Bulk Synchronous Parallel ML (BSML)

Past projects

Funded Projects

• 2022-2023: DeSSUF ― A Methodology for the Design of a Safe, Secure and User-Friendly Reactive Programming Language for the Internet of Things (45k€, funded by Université d'Orléans in the context of the Athena European University. Role: PI)
• 2015-2017: Big graphs: querying, mining and analysing (GIRAFON)
• 2011-2014: Parallel Program Development with Algorithmic Skeletons (PaPDAS)
• 2011-2013: High Performance Computing for Artifical Intelligence Applied to Finance (HPIAF) funded by EXQIM
• 2011-2013: Informatique en nuage: expérimentations et vérification (INEx)
• 2010-2012: Système de Programmation et d'Exécution Efficace de coDe sur architectures parallèles hétérogènes (SPEED)
• 2008-2009: BQR "Développement systématique de programmes parallèles certifiés" (Université d'Orléans)
• 2004-2007: the Propac project (ACI Jeunes Chercheuses et Chercheurs 2004)
• 2005: BQR CaPSyC "Calcul parallèle et simulation de systèmes complexes" (Université Paris XII Val-de-Marne)
• 2002-2004 : the CARAML project (ACI GRID 2001)

Software Projects

• 2018-2022: The Python Skeleton Library (PySke)
• 2018-2021: alloy2coq (alloy2coq)
• 2007-2014: Orléans Skeleton Library (OSL)
• 2004-2005: Departmental Metacomputing ML
• 2003-2008 : Minimally Synchronous Parallel ML (MSPML) /li>
• 2003: the BSFC++ library
• 1996-1998: the CDS* project

Former Postdoctoral Researchers

• Muath Alrammal (Assistant Professor at Khawarizmi International College, UAE)
• Vitor Rodrigues (Postdoctoral Researcher at Università degli Studi di Torino, Italy)
• Sunisa Rimchaoren (Assistant Professor at Burapha University, Thailand)

Former Students

• Former PhD students:
  1. Pr. Frédéric Gava (Full Professor, Université Paris Est Créteil, France)
  2. Dr. Louis Gesbert (Research Engineer, OCamlPro, France)
  3. Dr. Mohamad Al Hajj Hassan (Research Engineer, Huawei, Germany), supervised mainly by Dr. Mostafa Bamha
  4. Dr. Noman Javed (Postdoctoral Researcher, The London School of Economics and Political Science, UK)
  5. Dr. Julien Tesson (Research Engineer, Nomadic Labs, France)
  6. Dr. Joeffrey Légaux (Research Engineer, Centre Européen de Recherche et de Formation Avancée en Calcul Scientifique - CERFACS, Toulouse, France), co-supervised with Sylvain Jubertie
  7. Dr. Thomas Pinsard (Lecturer, Universit&eacuate; d'Orléans, France), co-supervised with Frédéric Dabrowski
  8. Dr. Sylvain Dailler (Research Engineer, Inria, France), co-supervised with Frédéric Dabrowski
  9. Dr. Asma Guesmi (supervised with Patrice Clemente and Pascal Berthomé)
  10. Dr. Allan Blanchard (Researcher, CEA, France), co-supervised with Nikolai Kosmatov
  11. Dr. Arvid Jakobsson (Research Engineer, Nomadic Labs, France) co-supervised with W. Bousdira, F. Dabrowski, W. Suijlen, G. Hains
  12. Dr. Thibaut Tachon (Research Engineer, Huawei Technologies, France), co-supervised with G. Hains
  13. Dr. Salwa Souaf (Postdoctoral Researcher, CEA, France), co-supervised with P. Berthomé
  14. Dr. Dara Ly (Engineer, Systerel) co-supervised with J. Signoles, N. Kosmatov and J.-M. Couvreur, CEA and LIFO
• Former Master students:
  • Dr. Myrto Arapinis (Reader, The University of Edinburgh, UK)
  • Dr. Abdeltouab Belbekkouche
  • David Billiet
  • Radia Benheddi (Senior Manager, National Bank of Canada)
  • Dr. Mohammad Charaf Eddin (Software Engineer, Telecom Paris, France
  • Dr. Frédéric Dabrowski (Associate Professor, Université d'Orléans, France)
  • Dr. Frédéric Gava (Full Professor, Université Paris Est, France)
  • Dr. Noman Javed (Postdoctoral Researcher, The London School of Economics and Political Science, UK)
  • Dimitri Louis-Régis (Implementation Manager, Webb Fontaine, Le Havre, France)
  • Dr. Armelle Merlin (Assistant Professor, Université de Toulouse, France)
  • Dr. Thomas Pinsard (Lecturer, Université d'Orléans, France)
  • Dr. Simon Robillard (Assistant Professor, University of Montpellier, France)
  • Dr. Julien Tesson (Research Engineer, Nomadic Labs, Paris, France)
  • Dr. Sylvain Dailler (Research Engineer, Inria, France)
  • Joris Rubagotti (Software Engineer, Sopria Steria, France)
  • Dr. Jolan Philippe (Postdoctoral Researcher, IMT Atlantique, Nantes, France), School of Informatics, Computing, and Cyber Systems, Northern Arizona University, USA
• Former Undergraduate Students:
  • Benjamin Gaudin, Université d'Orléans, France
  • Olivia Proust, Université d'Orléans, France
  • Terence Clastres, Université d'Orléans, France
  • Weiheng Su, School of Informatics, Computing, and Cyber Systems, Northern Arizona University, USA
  • Aurélien Plet, School of Informatics, Computing, and Cyber Systems, Northern Arizona University, USA
  • Christopher Whitney, School of Informatics, Computing, and Cyber Systems, Northern Arizona University, USA
  • Guillaume Petiot, Université d'Orléans, France

International and Young Researchers School Lectures

• April 2, 2015: cours «Calcul de programmes de parallèles en Coq» à l'École des jeunes chercheur/se/s en informatique mathématique (EJCIM 2015)
• October 29-November 28 2013: Lectures on Systematic Development of Correct Programs for Parallel and Cloud Computing, NII International advanced lectures series on ICT, Japan
• September 2007: Summer school organised by Institut de la francophonie pour l'informatique (IFI), Vietnam
• November 2004: Seminar “Últimos Avances en Informatíca”, La Laguna University, Tenerife, Spain

Organization and Program Chair

• Co-Program chair of the 14th International Symposium on High-Level Parallel Programming and Applications (HLPP 2021)
• Co-Program Chair of the 15th International Conference on Tests and Proofs (TAP 2021)
• Co-Program Chair of the track "Next Generation Programming Paradigms and Systems", 34th ACM SIGAPP Symposium on Applied Computing (NGPS@SAC 2019)
• Co-Program Chair of the IEEE International Conference on Scalable Computing and Communications (ScalCom 2018)
• Co-Program Chair of the IEEE International Conference on Scalable Computing and Communications (ScalCom 2017)
• 4PAD: Co-chair of the Special session Formal Approaches to Parallel and Distributed Systems (4PAD) at PDP 2016
• PAPP Workshops/Tracks:
  • Co-chair of the "Object Oriented and Parallel Programming Systems" track of ACM SAC 2018 (PAPP/OOPPS 2018)
  • Chair of the 11th event "Practical Aspects of High-Level Parallel Programming" as a track of ACM SAC 2017 (PAPP 2017)
  • Chair of the 10th event "Practical Aspects of High-Level Parallel Programming" as a track of ACM SAC 2016 (PAPP 2016)
  • Chair of the 9th international workshop on "Practical Aspects of High-Level Parallel Programming" (PAPP 2012)
  • Chair of the 8th international workshop on "Practical Aspects of High-Level Parallel Programming" (PAPP 2011)
  • Co-Chair and co-Organizer with Anne Benoit of the fifth international workshop on "aPplications of declArative and object-oriented Parallel Programming" (PAPP 2008)
  • Co-Chair and co-Organizer with Anne Benoit of the fifth international workshop on "aPplications of declArative and object-oriented Parallel Programming" (PAPP 2008)
  • Co-Chair and co-Organizer with Anne Benoit of the fourth international workshop on "Practical Aspects of High-Level Parallel Programming" (PAPP 2007)
  • Co-Chair and co-Organizer with Anne Benoit of the third international workshop on "Practical Aspects of High-Level Parallel Programming" (PAPP 2006)
  • Chair and Organizer of the second international workshop on "Practical Aspects of High-level Parallel Programming" (PAPP 2005)
  • Chair and Organizer of the first international workshop on "Practical Aspects of High-level Parallel Programming" (PAPP 2004)
• HLPP Workshops:
  • Chair and Organizer of the fourth international workshop on "High-Level Parallel Programming and Applications" (HLPP 2010) affiliated to the 15th ACM SIGPLAN International Conference on Functional Programming. Proceedings available in the ACM Digital Library
  • Co-Chair and co-Organizer with Alexandre Tiskin of the third international workshop on "High-Level Parallel Programming and Applications" (HLPP 2005)
  • Co-organizer and co-Chair with Gaétan Hains of the Second international workshop on "High-Level Parallel Programming and Applications" (HLPP 2003)
• Working groups and Informal Workshops:
  • The PaPDAS workshop / L'atelier PaPDAS, juillet 2014
  • The FraDeCoPP-3 workshop / L'atelier FraDeCoPP-3, octobre 2013
  • Deuxième Journée Informatique en Nuage à Orléans, janvier 2013 (JINO-2)
  • The FraDeCoPP-2 workshop / L'atelier FraDeCoPP-2, décembre 2012
  • Organisateur des Journées communes GdT LAC (GdR IM), LaMHA et LTP (GdR GPL) à Orléans, octobre 2012 (LLL)
  • Première Journée Informatique en Nuage à Orléans, juillet 2012 (JINO-1)
  • Rencontre de réflexion sur la recherche reproductible, Orléans, 5 avril 2012 (RRRR)
  • Head of the national working group LaMHA of the GDR GPL from 2008 to 2011
  • Journée du PPF Cascimodot du 18 novembre 2005

Guest editor

• Co-guest editor of a special issue of Formal Aspects of Computing on Tests and Proofs (TAP 2020 & 2021)
• Co-guest editor of a special issue of the Journal of Computer Languages on Languages for the IoT
• Co-guest editor of a special issue of the International Journal of Parallel Programming on High-Level Parallel Programming and Applications (HLPP 2021)
• Guest editor of a special issue of the Journal of Logical and Algebraic Methods in Programming on Formal Method for Parallel and Distributed Systems
• Special issue of Parallel Processing Letters (volume 18, issue 1, 2008) devoted to the HLPP 2005 workshop (with Alexander Tiskin)
• Special issue of Scalable Computing: Practice and Experience (volume 8, issue 4, 2007), selected extended and revised papers from PAPP 2006 the second workshop on Practical Aspects of High-Level Parallel Programming (with Anne Benoit)
• Special issue of Computer Languages, Systems and Structures on Semantics and Cost Models for High-Level Parallel Programming, volume 33, issue 3-4, 2007
• Special issue of Scalable Computing: Practice and Experience, selected extended and revised papers from the second workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2005), September 2006
• Special issue of Scalable Computing: Practice and Experience, selected extended and revised papers from the first Practical Aspects of High-Level Parallel Programming workshop (PAPP 2004)
• Special issue of Parallel Processing Letters (volume 13, issue 3, 2003) devoted to the HLPP 2003 workshop (with Gaétan Hains)

Programme committee member

• International Conference on Computational Science (ICCS 2024)
• 19th International Conference on Integrated Formal Methods (iFM 2024)
• ACM Symposium on Applied Computing - Track Software Verification and Testing (SAC/SVT 2024)
• International Conference on Computational Science (ICCS 2023)
• International Conference on Computational Science (ICCS 2022)
• International Conference on Computational Science (ICCS 2021)
• ACM Symposium on Applied Computing - Track Software Verification and Testing (SAC/SVT 2021)
• International Symposium on High Level Parallel Programming and Applications (HLPP 2020)
• International Conference on Computational Science (ICCS 2020)
• ACM Symposium on Applied Computing - Track Software Verification and Testing (SAC/SVT 2020)
• International Conference on Computational Science (ICCS 2019)
• International Conference on High Performance Computing and Simulation (HPCS 2019)
• International Conference on Computational Science (ICCS 2018)
• International Conference on High Performance Computing and Simulation (HPCS 2018)
• International Conference on Computational Science (ICCS 2018)
• International Conference on High Performance Computing and Simulation (HPCS 2017)
• International Conference on Computational Science (ICCS 2017)
• Journées Francophones des Langages Applicatifs (JFLA 2017)
• Special session Formal Approaches to Parallel and Distributed Systems (4PAD) at PDP 2017
• Seventh International Conference on Interactive Theorem Proving (ITP 2016)
• International Conference on Computational Science (ICCS 2016)
• International Conference on Computational Science (ICCS 2015)
• 16th International Conference on High Performance Computing and Communications (HPCC 2014)
• 16th Workshop on Advances in Parallel and Distributed Computational Models (APDCM 2014)
• International Conference on Computational Science (ICCS 2014)
• International Conference on Computational Science (ICCS 2013)
• International Conference on Computational Science (ICCS 2012)
• International Conference on Computational Science (ICCS 2011)
• Workshop on High-Performance and Distributed Computing for Financial Applications (HPDFA 2010)
• 6th International Workshop on aPpplications of declArative and object-oriented Parallel Programming (PAPP 2009)
• 20th International Symposium on the Implementation and Application of Functional Languages (IFL 2008)
• 9th International Conference on Software Engineering Research, Management and Applications (SERA'08)
• 9th International Conference on Parallel Computing Technologies (PaCT'07)
• 18th International Workshop on Implementation and Application of Functional Languages (IFL'06)
• 17th International Workshop on Implementation and Application of Functional Languages (IFL'05)
• Workshop on Language-Based Parallel Programming Models (WLPP)
• Journées Francophones des Langages Applicatifs (JFLA 2005)
• 16th International Workshop on Implementation and Application of Functional Languages (IFL'04)

PhD Committees

2024

• Darine Rammal, Université d'Orléans, France, January 2024 (member)
  Memory Safety for Synchronous Reactive Programming

2023

• Clément Pascutto, Université Paris Saclay, France, October 2023 (reviewer)
  Runtime Verification of OCaml Programs

2022

• Dara Ly, Université d'Orléans, France, December 2022 (advisor)
  Formalization of a Runtime Assertion Checker for Memory Properties of C Programs
• Virgile Robles, Université Paris Saclay, France, January 2022 (reviewer)
  Specifying and verifying high-level requirements on large programs : application to security of C programs

2020

• Salwa Souaf, INSA Centre Val-de-Loire, December 2020 (advisor)
  Formal Methods Meet Security in a Cost Efficient Cloud Brokerage Solution

2019

• Arvid Jakobsson, Université d'Orléans, France, June 2019 (advisor)
  Static Analysis for BSPlib Programs
• Thibaut Tachon, Université d'Orléans, France, June 2019 (advisor)
  Automatic Generation of BSP Code

2018

• Jean-Christophe Léchenet, Université Paris-Saclay, July 2018 (member)
  Certified Algorithms for Program Slicing

2016

• Allan Blanchard, Université d'Orléans, December 2016 (advisor)
  Verification of concurrent programs assisted by code and specification transformation
• Asma Guesmi, Université d'Orléans, July 2016 (advisor)
  Spécification et analyse formelles des politiques de sécurité dans un processus de courtage de l'informatique en nuage
• Etienne Brodu, INSA Lyon, June 2016 (reviewer)
  Fluxional compiler: seamless shift from development productivity to performance efficiency

2015

• Sylvain Dailler, Université d'Orléans, 2015 (advisor)
  Extension paramétrée de compilateur certifié pour la programmation parallèle
• Antoine Tran Tan, Université Paris-Sud, 2015 (reviewer)
  Squelettes algorithmiques asynchrones: application aux langages orientés domaine

2014

• Mouhamadou Sakho, Université d'Orléans, December 2014 (chair)
  Gamma-pomset pour la modélisation et la vérification de systèmes parallèles
• Thomas Pinsard, Université d'Orléans, December 2014 (advisor)
  Nested Atomic Sections with Thread Espace: Semantics and Compilation
• Nuno Gaspar, Université de Nice, December 2014 (reviewer)
  Mechanized support for the formal specification, verification, and deploiement of component-based applications
• Nader Khammassi, ENSTA Bretagne, December 2014 (reviewer)
  High-Level Structured Programming Models For Explicit and Automatic Parallelization on Multicore Architectures
• Charif Mahmoudi, Université Paris-Est Créteil, November 2014 (reviewer)
  Orchestration d'agents mobiles en communauté
• Hélène Coullon, Université d'Orléans, September 2014 (chair)
  Modélisation et implémentation de parallélisme implicite pour les simulations scientifiques basées sur des maillages

2013

• Joeffrey Légaux, Université d'Orléans, December 2013 (advisor)
  Squelettes algorithmiques pour la programmation et l'exécution efficaces de codes parallèles
• Chong Li, Université Paris-Est, July 2013 (chair)
  Un modèle de transition logico-matérielle pour la simplification de la programmation parallèle

2011

• Hiep-Thuan Do, Université d'Orléans, December 2011
  Extensibilité des moyens de traitements pour les données issues des vastes systèmes d'informations géographiques
• Julien Tesson, Université d'Orléans, November 2011 (advisor)
  Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels
• Khaled Hammidouche, Université Paris Sud, November 2011 (reviewer)
  Programmation des machines hiérarchiques et hétérogènes
• Noman Javed, Université d'Orléans, October 2011 (advisor)
  Squelettes algorithmiques méta-programmés : implantations, performances et sémantique

2009

• Mohamad Al Hajj Hassan, Université d'Orléans, December 2009 (advisor)
  Parallélisme et équilibrage de charges dans le traitement de la jointure sur des architectures distribuées
• Mâamoun Bernichi, Université Paris-Est, November 2009
  Sécurité logicielle à base d'une communauté d'agents mobiles
• Louis Gesbert, Université Paris-Est, March 2009 (advisor)
  Développement systématique et sûreté d'exécution en programmation parallèle structurée

2005-2008

• Mario Leyton, Université de Nice, October 2008 (reviewer)
  Advanced Features for Algorithmic Skeleton Programming
• Frédéric Dabrowski, Université Denis Diderot, June 2007 (chair)
  Programmation réactive synchrone
• Joel Falcou, Université Blaise Pascal, December 2006 (reviewer)
  Un cluster pour la vision temps réel: architecture, outils et applications
• Frédéric Gava, Université Paris 12 Val-de-Marne, December 2005 (advisor)
  Approches fonctionnelles de la programmation parallèle et des méta-ordinateurs. Sémantiques, implantations et certification
• Mehdi Ammi, Université d'Orléans, December 2005
  Interface Homme-Machine Multimodale pour la Télé-Micromanipulation

Past Working Groups

• 2005 : groupe de travail "Parallélisme et vérification"
• 2001-2003 : SLOVO (GDR-ALP, CNRS)
• 2001 : Algorithmic Skeletons Standardisation Project
• 2000-2001 : LACL's working group
• 1999 : PRO (Parallélisme, répartition et objets) "Architecture objet évolutive pour le calcul parallèle sur les tableaux"
• 1998-1999 : LODEC