معرفی
David Monniaux is a senior researcher (directeur de recherche) at CNRS, the largest French national scientific research agency. He works at VERIMAG, a computer science laboratory jointly operated by CNRS and the University of Grenoble. His research focuses on proving software correct, connecting to computability theory, complexity theory, and mathematical logic.
Dr. Monniaux holds a PhD in Computer Science (2001, Université Paris Dauphine) and a habilitation in Computer Science (2009, Université Joseph Fourier, Grenoble), as well as an agrégation in mathematics.
His research interests span programming languages, static analysis, model checking, compilers, and assisted proof. He has particular expertise in proving strong properties of critical software used in civil aviation, especially regarding numerical overflows and floating-point computations. He has also worked on cryptographic protocols and probabilistic systems. His approach combines abstract interpretation, formal verification, and mathematical logic to address software correctness problems.
Dr. Monniaux's recent work shows a strong focus on static analysis techniques, program verification, and formal methods. His publications demonstrate expertise in polyhedral analysis, strategy iteration, and the application of SMT solving to program analysis problems. His research bridges theoretical computer science with practical applications in safety-critical systems.
Among his notable scientific contributions are projects like VERASCO (integrating static analysis into the CompCert certified compiler), STATOR (exploring advanced techniques for automatic inference of program invariants), and ASOPT (developing new algorithms for static program analysis).
Dr. Monniaux has advised several students who have gone on to successful careers, including Julien Henry (now at Grammatech), Alexis Fouilhé (now in industry), George (Egor) Karpenkov (now at Apple Inc.), and Alexandre Maréchal (post-doctoral researcher at LIP6). He currently advises Hang Yu and Valentin Touzeau.
He is actively involved in the programming languages and formal methods research community, serving on program committees for major conferences including POPL, PLDI, and VMCAI.
