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.
STATOR is a European Research Council (ERC) starting investigator (consolidator) grant.
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.
See also download subdirectory for odds and ends.
The preferred way to contact me is by email to
David.Monniaux AT univ-grenoble-alpes.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/C371AAD0 2017-01-13 [expires: 2022-01-12] Key fingerprint = D671 CC22 03A6 5156 1C32 9AC4 A3C2 E122 C371 AAD0
My snail mail address is:
Université Grenoble Alpes
700, avenue centrale
38401 Saint Martin d’Hères
I write a blog, mostly in French, but sometimes also in English.