David Monniaux

I'm a researcher of the National Center for Scientific Research (CNRS), VERIMAG laboratory. I am also part-time associate professor at École Polytechnique.

If this matters to you (PhD committees and so on), I hold an habilitation in computer science.

Work

Research

See my publications (and also my list on HAL).

Interests

I've been interested in

• cryptography, and more specifically to large number factoring (see my internship report on a factoring method using lattice reduction)
• proof systems in higher-order logics, especially through Curry-Howard isomorphism (calculus of inductive constructions...)
• abstract interpretation, with Patrick Cousot
• the analysis of cryptographic protocols through abstract interpretation.
• the analysis of probabilistic programs by abstract interpretation (PhD topic).

My main current research area is static analysis by abstract interpretation of software, in particular to find possible run-time errors. I was involved, among others, in the conception and programming of the ASTRÉE static analyzer, used to check the critical software of the fly-by-wire controls at Airbus.

Software

In addition to involvements in various software projects, I now maintain:

• Mjollnir, a quantifier elimination tool for the theory of linear inequalities

• gnytool, a decision procedure for GNY logic (see here)

Participation in research projects

Current

• ANR ASOPT

Past

• RNTL ASTREE, produisant notamment l'analyseur statique Astrée - statically and automatically prove the absence of run-time errors in critical embedded real-time software.
• DAEDALUS - analysis of computing systems embedded in aircraft.
• Probabilistic static analysis, in cooperation with the French atomic energy agency (CEA).

Teaching

• École Polytechnique (my page there)
• Université de la Réunion:

Miscellaneous

• See also my page of links.
• My programs.

These WWW pages have been written, as long as possible, in standard HTML. They are designed so that they are displayed correctly in any standard-compliant navigator, while featuring a pleasant look for people who have graphical navigators.

My email address here is David.MonniauxZOINX@imag.fr (remove the ZOINX, which is a trap for address-collecting robots run by senders of unsolicited commercial e-mail.