Research
Current research interests
Correctness of program and component software properties
obtained by construction via language design or derivation from
specifications, or obtained a posteriori by static analysis or
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).
Students
- PhD students:
- 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
- 2023-2025: 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)
-
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
- 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)
-
2018-2022: The Python Skeleton Library
(PySke)
-
2018-2021: alloy2coq
(alloy2coq)
- 2015-2017:
Big graphs: querying, mining and analysing
(GIRAFON)
-
2007-2014: Orléans Skeleton Library
(OSL)
- 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)
- 2004-2005: Departmental Metacomputing ML
-
2003-2008 :
Minimally Synchronous Parallel ML
(MSPML)
-
2002-2004 :
the CARAML project
(ACI GRID 2001)
- 2003:
the BSCF++ 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:
-
Pr. Frédéric Gava
(Full Professor, Université Paris Est
Créteil, France)
-
Dr. Louis
Gesbert (Research
Engineer, OCamlPro,
France)
-
Dr. Mohamad Al Hajj Hassan (Research Engineer, Huawei,
Germany), supervised mainly by
Dr. Mostafa
Bamha
-
Dr. Noman Javed (Postdoctoral Researcher, The London
School of Economics and Political Science, UK)
-
Dr. Julien Tesson
(Research Engineer, Nomadic Labs, France)
-
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
-
Dr. Thomas Pinsard (Lecturer, Universit&eacuate;
d'Orléans, France), co-supervised with
Frédéric Dabrowski
-
Dr. Sylvain Dailler (Research Engineer, Inria, France),
co-supervised with Frédéric Dabrowski
-
Dr. Asma Guesmi (supervised with Patrice Clemente and
Pascal Berthomé)
-
Dr. Allan
Blanchard (Researcher, CEA, France), co-supervised
with Nikolai Kosmatov
- Dr. Arvid Jakobsson (Research Engineer, Nomadic Labs,
France) co-supervised with W. Bousdira, F. Dabrowski,
W. Suijlen, G. Hains
- Dr. Thibaut Tachon (Research Engineer, Huawei
Technologies, France), co-supervised with G. Hains
- Dr. Salwa Souaf (Postdoctoral Researcher, CEA, France),
co-supervised with P. Berthomé
- 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
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:
-
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
- 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
- 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
2023
- Clément Pascutto, Université Paris Saclay, France,
October 2023 (reviewer)
Runtime Verification of OCaml Programs
2022
2020
- Salwa Souaf, INSA Centre Val-de-Loire, December 2020 (advisor)
Formal Methods Meet Security in a Cost Efficient Cloud Brokerage Solution
2019
2018
-
Jean-Christophe Léchenet, Université Paris-Saclay, July 2018 (member)
Certified Algorithms for Program Slicing
2016
2015
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
2011
2009
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