I am senior researcher (*directeur de recherche*) at CNRS, the largest French national scientific research agency.
I work at VERIMAG, a computer science laboratory jointly operated by CNRS and the University of Grenoble.

The practical focus of my research is how to prove software correct. This is connected to computability theory, since software correctness, in general, is an undecidable problem, to complexity theory, since many verification problems have high complexity, to mathematical logic, and to fields as diverse as game theory, algebra, and convex optimization.

I've been interested, in particular, in proving strong properties of critical software used in civil aviation (e.g. with respect to numerical overflows and floating-point computations). I've also worked on cryptographic protocols and probabilistic systems.

I hold a PhD (2001, Université Paris Dauphine) and habilitation in computer science (2009, Université Joseph Fourier, Grenoble), as well as an *agrégation* in mathematics.

A list of my publications, with links to downloadable copies, may be found here. You may also wish to consult my entry at DBLP.

The VERASCO project aims at integrating a static analyzer into the CompCert certified compiler, and prove it correct with the Coq system. The VERIMAG component focuses on numerical invariants.

VERASCO is funded by the French National agency for research (ANR). See our wiki for more detail.

I am principal investigator for STATOR, which explores advanced techniques for automatic inference of program invariants (abstract interpretation, SMT-solving etc.).

STATOR is a European Research Council (ERC) starting investigator (consolidator) grant.

STATOR is recruiting! Please see our job offers for postdocs, funded PhDs, and even masters internships! All enquiries should be directed to me.

The ASOPT (* Analyse Statique et optimisation*) project developed new algorithms for static program analysis, in particular by bringing in techniques from mathematical optimization and game theory.

Astrée is a static analysis tool, which takes C programs as input and attempts proving that no undefined behaviors (overflows, array-out-of-bound errors, bad pointer dereferencing etc.) or other undesirable conditions (assertion violations) can occur. It does so by computing program invariants and checking that they entail the desired conditions.

Astrée is used in avionics, automotive and other industrial applications and is sold through Absint GmbH.

- Julien Henry (now in industry)
- Alexis Fouilhé (now in industry)

- George (Egor) Karpenkov
- Alexandre Maréchal

The preferred way to contact me is by email to `David.Monniaux AT imag.fr`

. Otherwise, you can try phoning my office at **+33 4 57 42 22 32**; beware that I may be unavailable. Should you need it, the lab has a shared fax number +33 4 57 42 22 22. My current GPG key is:

pub 4096R/DACE1A0A 2012-02-02 [expires: 2017-01-31] Key fingerprint = B50C 2918 7E7C 4AA7 A12A 18FA 5DAE 1C35 DACE 1A0A uid David Monniaux <David.Monniaux@imag.fr> sub 4096R/0B47892B 2012-02-02 [expires: 2017-01-31]

My snail mail address is:

VERIMAG

Bâtiment IMAG

Université Grenoble Alpes

700, avenue centrale

38401 Saint Martin d’Hères

France

I write a blog, mostly in French, but sometimes also in English.

David Monniaux AT imag.fr