IRIT - UMR 5505

English
UPS
  Bandeau IRIT
 
Photo EMD

Érik Martin-Dorel

Statut : 
Maître de Conférences
E-mail : 
erikREMOVETHIS.martin-dorel@REMOVETHATirit.fr
Localisation : 
UPS / IRIT2 / Niveau 4, Pièce : 473
Téléphone : 
05 61 55 6416
Publications : 

 

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 1er 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 1er 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 (2022-2023)

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-encadrement (avec Hélène Fargier) de la thèse de doctorat de Pierre Pomeret-Coquot (2020-2023, bourse MESR/ED-MITT)

 

Haut de page

 

Enseignement

UPS
Département Info
Depuis septembre 2014, j'effectue mon service d'enseignement dans le Département Informatique de la Faculté des Sciences et d'Ingénierie de l'UPS, au niveau Licence et Master.
Master DL En particulier, je fais partie du comité de pilotage du Master DL pour lequel j'effectue une partie significative de mon service d'enseignement.

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

 

Haut de page