Érik Martin-Dorel

 

Recherche

Thèmes de recherche

Les mots-clés suivants résument mes principaux thèmes de recherche:

• méthodes formelles : assistants de preuve formelle (Coq, SSReflect, PVS), formalisation des mathématiques, théorie des types, théorie de la démonstration, logiques classique et intuitionniste, spécifications formelles, vérification formelle, certificats ;
• méthodes numériques : arithmétique des ordinateurs, arithmétique en virgule flottante, arrondi correct, approximation polynomiale certifiée, arithmétique par intervalles, optimisation globale, calcul formel ;
• théorie des jeux : preuve formelle pour la théorie des jeux : formalisation de jeux booléens, jeux déterminés, jeux en forme normale...
• génie logiciel : CI/CD, automatisation de tests, de chaînes de V&V ou de livraison continue...

Recherches actuelles

Mes activités de recherche se focalisent sur les applications de la preuve formelle interactive, en particulier pour la vérification formelle de résultats en arithmétique des ordinateurs et en théorie des jeux.

Je m'intéresse également à la conception de méthodes pour accroître l'automatisation des preuves dans les assistants de preuve formelle, et aussi à l'automatisation de tests en général et spécifiquement autour de l'outillage de projets de la communauté OCaml et Coq.

Parcours de recherche

Depuis le 1^er septembre 2014, je suis Maître de Conférences à l'Université Toulouse III – Paul Sabatier et je conduis mes activités de recherche dans l'équipe ACADIE de l'IRIT.

Précédemment, j'étais post-doctorant dans l'équipe VALS/Toccata du LRI (UMR 8623 CNRS & Université Paris-Sud) à l'Inria Saclay - Île-de-France en tant que membre du projet VERASCO de l'ANR.

Auparavant, j'étais post-doctorant dans l'équipe-projet Marelle d'Inria Sophia Antipolis en tant que membre du projet TaMaDi de l'ANR.

J'ai soutenu ma thèse de doctorat le 26 septembre 2012 à l'ENS de Lyon, où je travaillais dans l'équipe-projet AriC (ex-Arénaire) au LIP, sous la direction conjointe de Jean-Michel Muller et Micaela Mayero.

Mon manuscrit de thèse et mes transparents de soutenance sont disponibles en ligne.

Exposés

Certified, Efficient and Sharp Univariate Taylor Models in COQ à SYNASC 2013.

Formal proofs and certified computation in Coq à Games 2015.

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq à FAC 2016.

A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations à CPP 2017.

An Existence Theorem of Nash Equilibrium in Coq and Isabelle à GandALF 2017 (code).

The under tactic (math-comp meeting, 2019-02-28)

SSReflect in Coq 8.10 au Workshop Coq 2019 (Demo)

Primitive Floats in Coq à ITP 2019

Overview of the recent and upcoming features of Learn-OCaml (GT Learn-OCaml, 2022-03-23)

Learn-OCaml: How to contribute? (GT Learn-OCaml, 2022-03-23)

Overview of the PFITAXEL project Using the Learn-OCaml platform (DAS e-education@IRIT, 2022-05-20)

Exposé Learn-OCaml au 1^er Meetup Toulouse OCaml UserS (2022-10-11)

Hardware floating-point computations in Coq à Certified and Symbolic-Numeric Computation (ENS de Lyon, 2023-05-26)

Sujets de stage / projet / thèse (2024-2025)

• Sujet de M2 Info : Développement web pour learn-ocaml : authentification modulaire et maintenance corrective/évolutive (sujet pourvu)
• Sujet de M1 Info : Développement web pour learn-ocaml : fonctionnalité d'authentification et utilisation du protocole LTI (sujet pourvu)

Si vous avez un intérêt prononcé pour un des thèmes de recherche que j'ai mentionnés mais qu'aucun sujet de stage là-dessus ne figure actuellement, n'hésitez pas à me contacter et m'envoyer un CV+LM, pour discuter d'une possibilité de stage avec moi dans l'équipe ACADIE.

Encadrement de thèse

• Co-direction (avec Hélène Fargier) de la thèse de doctorat de Pierre Pomeret-Coquot (2020-2023, bourse MESR/ED-MITT)

 

 

Enseignement

Plus précisément, je suis intervenu dans les modules suivants (dans l'ordre antichronologique) :

• 2017-2018
  • PFITA, TAPFA (L3, UPS)
  • ComFlex, DeQo-GeCo, Java EE, WebX (M1 DL, UPS)
  • IVVQ (M2 DL, UPS)
  • VC (M2 CSA, UPS)
• 2016-2017
  • PFITA, TAPFA (L3, UPS)
  • ComFlex, DeQo-GeCo, Java EE, WebX (M1 DL, UPS)
  • IVVQ (M2 DL, UPS)
• 2015-2016
  • PF1 (L3, UPS)
  • AL, DCLL, IAWS, Java EE (M1 DL, UPS)
  • IVVQ (M2 DL, UPS)
• 2014-2015
  • AL, DCLL, IAWS, Java EE (M1 DL, UPS)
• 2013-2014
  • « TP de Programmation orientée objet en Java – S2-POO (niveau L1) » avec Jean-Claude Martin à l'IUT d'Orsay.
  • « TP d'Objets répartis pour la licence professionnelle PER (niveau L3) » avec Andrei Paskevich et Karl-Eduard Berger à l'IUT d'Orsay.
  • « Projet tutoré Java/Android pour la licence professionnelle PER (niveau L3) » avec Andrei Paskevich à l'IUT d'Orsay.
• 2011-2012
  • « TD/TP d'Algorithmique et Programmation procédurale – LIF5 (niveau L2) » avec Samir Akkouche à l'UCBL.
  • « TD d'Architecture matérielle et logicielle – LIF6 (niveau L2) » avec Nicolas Louvet à l'UCBL.
• 2010-2011
  • « TP d'Algorithmique, Programmation et Complexité – LIF9 (niveau L3) » avec Julien Mille et Ricardo Uribe Lobello à l'UCBL.
• 2009-2010
  • « TD de Preuve assistée par ordinateur avec Coq (niveau M1) » avec Jean Duprat et Aurélien Pardon à l'ENS de Lyon.
  • « TP de Programmation fonctionnelle et récursive en Scheme – LIF3 (niveau L1) » avec Nathalie Guin à l'UCBL.
  • « TP d'Algorithmique et programmation impérative – LIF1 (niveau L1) » avec Élodie Desseree à l'UCBL.