| 2026 | ESOP | Max-Policy Iteration, Revisited. | David Monniaux, Helmut Seidl |
| 2025 | CPP | Formally Verified Hardening of C Programs against Hardware Fault Injection. | Basile Pesin, Sylvain Boulm, David Monniaux, Marie-Laure Potet |
| 2024 | CPP | Memory Simulations, Security and Optimization in a Verified Compiler. | David Monniaux |
| 2023 | TAP | Testing a Formally Verified Compiler. | David Monniaux, Lo Gourdin, Sylvain Boulm, Olivier Lebeltel |
| 2022 | ARITH | Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic. | David Monniaux, Alice Pain |
| 2022 | CPP | Formally verified superblock scheduling. | Cyril Six, Lo Gourdin, Sylvain Boulm, David Monniaux, Justus Fasse, Nicolas Nardino |
| 2022 | ESOP | The Trusted Computing Base of the CompCert Verified Compiler. | David Monniaux, Sylvain Boulm |
| 2022 | FMCAD | BaxMC: a CEGAR approach to Max#SAT. | Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet |
| 2021 | SAS | Data Abstraction: A General Framework to Handle Program Verification of Data Structures. | Julien Braine, Laure Gonnord, David Monniaux |
| 2019 | ICCS | Parallel Parametric Linear Programming Solving, and Application to Polyhedral Computations. | Camille Coti, David Monniaux, Hang Yu |
| 2019 | SAS | An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection. | Hang Yu, David Monniaux |
| 2018 | SAS | Extending Constraint-Only Representation of Polyhedra with Boolean Constraints. | Alexey Bakhirkin, David Monniaux |
| 2018 | SYNASC | The Verified Polyhedron Library: an Overview. | Sylvain Boulm, Alexandre Marchal, David Monniaux, Michal Prin, Hang Yu |
| 2017 | CAV | Ascertaining Uncertainty for Efficient Exact Cache Analysis. | Valentin Touzeau, Claire Maza, David Monniaux, Jan Reineke |
| 2017 | SAS | Combining Forward and Backward Abstract Interpretation of Horn Clauses. | Alexey Bakhirkin, David Monniaux |
| 2017 | SAS | Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. | Alexandre Marchal, David Monniaux, Michal Prin |
| 2016 | CASC | A Survey of Satisfiability Modulo Theory. | David Monniaux |
| 2016 | SAS | Cell Morphing: From Array Programs to Array-Free Horn Clauses. | David Monniaux, Laure Gonnord |
| 2016 | VMCAI | Program Analysis with Local Policy Iteration. | Egor George Karpenkov, David Monniaux, Philipp Wendler |
| 2016 | VMCAI | Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem. | Alexandre Marchal, Alexis Fouilh, Tim King, David Monniaux, Michal Prin |
| 2015 | PLDI | Synthesis of ranking functions using extremal counterexamples. | Laure Gonnord, David Monniaux, Gabriel Radanne |
| 2015 | SAC | Polyhedra to the rescue of array interpolants. | Francesco Alberti, David Monniaux |
| 2015 | SAS | A Simple Abstraction of Arrays and Maps by Program Translation. | David Monniaux, Francesco Alberti |
| 2014 | SAS | Speeding Up Logico-Numerical Strategy Iteration. | David Monniaux, Peter Schrammel |
| 2013 | ITP | Implementing Hash-Consed Structures in Coq. | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
| 2013 | SAS | Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. | Alexis Fouilh, David Monniaux, Michal Prin |
| 2012 | CADE | Experiments on the feasibility of using a floating-point simplex in an SMT solver. | Diego Caminha Barbosa De Oliveira, David Monniaux |
| 2012 | CADE | Anatomy of Alternating Quantifier Satisfiability (Work in progress). | Anh-Dung Phan, Nikolaj S. Bjrner, David Monniaux |
| 2012 | SAS | Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation. | Julien Henry, David Monniaux, Matthieu Moy |
| 2011 | APLAS | Modular Abstractions of Reactive Nodes Using Disjunctive Invariants. | David Monniaux, Martin Bodin |
| 2011 | ESOP | Improving Strategies via SMT Solving. | Thomas Martin Gawlitza, David Monniaux |
| 2011 | ITP | On the Generation of Positivstellensatz Witnesses in Degenerate Cases. | David Monniaux, Pierre Corbineau |
| 2011 | SAS | Using Bounded Model Checking to Focus Fixpoint Iterations. | David Monniaux, Laure Gonnord |
| 2010 | CAV | Quantifier Elimination by Lazy Model Enumeration. | David Monniaux |
| 2009 | CAV | On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. | David Monniaux |
| 2009 | POPL | Automatic modular abstractions for linear constraints. | David Monniaux |
| 2008 | LPAR | A Quantifier Elimination Algorithm for Linear Real Arithmetic. | David Monniaux |
| 2007 | EMSOFT | Verification of device drivers and intelligent controllers: a case study. | David Monniaux |
| 2007 | SAS | Optimal Abstraction on Real-Valued Programs. | David Monniaux |
| 2007 | TASE | Varieties of Static Analyzers: A Comparison with ASTREE. | Patrick Cousot, Radhia Cousot, Jrme Feret, Antoine Min, Laurent Mauborgne, David Monniaux, Xavier Rival |
| 2005 | APLAS | The Parallel Implementation of the Astre Static Analyzer. | David Monniaux |
| 2005 | CAV | Compositional Analysis of Floating-Point Linear Numerical Filters. | David Monniaux |
| 2005 | ESOP | The ASTRE Analyzer. | Patrick Cousot, Radhia Cousot, Jrme Feret, Laurent Mauborgne, Antoine Min, David Monniaux, Xavier Rival |
| 2003 | PLDI | A static analyzer for large safety-critical software. | Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jrme Feret, Laurent Mauborgne, Antoine Min, David Monniaux, Xavier Rival |
| 2003 | SAS | Abstract Interpretation of Programs as Markov Decision Processes. | David Monniaux |
| 2003 | VMCAI | Abstraction of Expectation Functions Using Gaussian Distributions. | David Monniaux |
| 2001 | ESOP | Backwards Abstract Interpretation of Probabilistic Programs. | David Monniaux |
| 2001 | POPL | An abstract Monte-Carlo method for the analysis of probabilistic programs. | David Monniaux |
| 2001 | SAS | An Abstract Analysis of the Probabilistic Termination of Programs. | David Monniaux |
| 2000 | SAS | Abstract Interpretation of Probabilistic Semantics. | David Monniaux |
| 1999 | SAS | Abstracting Cryptographic Protocols with Tree Automata. | David Monniaux |