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 : formalisation de jeux booléens, de jeux en forme normale...

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.

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.

 

Haut de page

 

Enseignement

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.

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

 

Haut de page