Presentation

Je suis directeur de recherche au CNRS. Je travaille à VERIMAG, unité mixte de recherche du CNRS et de l'Université de Grenoble.

L'objectif pratique de ma recherche est de prouver la correction des logiciels. Ceci est relié à la théorie de la calculabilité, puisque la correction des logiciels, en général, est un problème indécidable, à la théorie de la complexité, puisque de nombreux problèmes de vérification sont de haute complexité, à la logique mathématique, et à des champs aussi divers que la théorie des jeux, l'algèbre, et l'optimisation convexe.

Je me suis notamment intéressé à prouver des propriétés de logiciels critiques utilisés en aviation civil (notamment par rapport aux dépassements de capacité arithmétique et des calculs en virgule flottante). J'ai égalemment travaillé sur les protocoles cryptographiques et les systèmes probabilistes.

Je suis titulaire du doctorat (2001, Université Paris Dauphine) et de l'habilitation à diriger les recherches (2009, Université Joseph Fourier, Grenoble), en informatique, et de l'agrégation de mathématiques.

Une liste de mes publications, avec des liens vers des versions téléchargeables, se trouve ici. Vous pouvez également vouloir consulter mon entrée sur DBLP.

Projets de recherche

En cours

VERASCO (2012–2015)

Le projet VERASCO vise à intégrer un analyseur statique dans le compilateur certifié CompCert, et le prouver correct dans l'assistant de preuve Coq. L'équipe de VERIMAG s'intéresse plus particulièrement aux invariants numériques.

VERASCO est financé par l'Agence nationale de la Recherche (ANR). Voir le wiki pour plus de détails.

STATOR (2012–2017)

Je suis le responsable du projet STATOR, qui porte sur les techniques avancées d'inférence d'invariants de programme.

STATOR est un projet du Conseil européen de la Recherche.

Offres d'emploi

STATOR recrute ! Voir nos offres de recrutement en post-doctorat, et doctorat (financé), stages etc. S'adresser à moi pour tout renseignement.

Achevés

ASOPT (2009–2012)

Le projet ASOPT (Analyse Statique et optimisation) a développé de nouveaux algorithmes d'analyse de programmes, notamment par utilisation de techniques issues de la recherche opérationnelle (optimisation) et de la théorie des jeux.

ASTRÉE

Astrée est un outil d'analyse statique, prenant en entrée des programmes en langage C et qui tente de prouver l'absence de comportement indéfini (dépassement de capacité, accès en dehors des bornes de tableaux, accès via des pointeurs invalides etc.) ou d'autres conditions indésirables (violations d'assertion). Il arrive ce résultat en calculant des invariants de programme et en vérifiant qu'ils impliquent la condition désirée.

Astrée est utilisé dans des applications avioniques, automobiles et industrielles et est commercialisé par Absint GmbH.

Doctorants

Passés

Actuels

Logiciels

Voir aussi le répertoire download.

Contact

La meilleur façon de me contacter est par courrier électronique à David.Monniaux AT univ-grenoble-alpes.fr. Vous pouvez également tenter de me téléphoner au +33 4 57 42 22 32; beware that I may be unavailable. Le numéro du télécopieur partagé du laboratoire est +33 4 57 42 22 22. Ma clef PGP actuelle est :

pub   4096R/C371AAD0 2017-01-13 [expires: 2022-01-12]
      Key fingerprint = D671 CC22 03A6 5156 1C32  9AC4 A3C2 E122 C371 AAD0
  

Mon adresse postale est :
VERIMAG
Bâtiment IMAG
Université Grenoble Alpes
700, avenue centrale
38401 Saint Martin d’Hères
France

Autres

Mon blog (extra-professionnel).

David Monniaux AT imag.fr