Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief. - David Monniaux (CSFW, 1999)

Abstract Interpretation of Probabilistic Semantics. - David Monniaux (SAS, 2000)

Backwards Abstract Interpretation of Probabilistic Programs. - David Monniaux (ESOP, 2001)

An abstract Monte-Carlo method for the analysis of probabilistic programs. - David Monniaux (POPL, 2001)

An Abstract Analysis of the Probabilistic Termination of Programs. - David Monniaux (SAS, 2001)

Analysis of probabilistic programs by abstract interpretation. (Analyse de programmes probabilistes par interprétation abstraite). - David Monniaux (2001)

Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. - Bruno Blanchet; Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; David Monniaux; Xavier Rival (The Essence of Computation, 2002)

A static analyzer for large safety-critical software. - Bruno Blanchet; Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; David Monniaux; Xavier Rival (PLDI, 2003)

Abstraction of Expectation Functions Using Gaussian Distributions. - David Monniaux (VMCAI, 2003)

Abstracting cryptographic protocols with tree automata. - David Monniaux (Sci. Comput. Program., 2003)

The Parallel Implementation of the Astrée Static Analyzer. - David Monniaux (APLAS, 2005)

Compositional Analysis of Floating-Point Linear Numerical Filters. - David Monniaux (CAV, 2005)

The ASTREÉ Analyzer. - Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; David Monniaux; Xavier Rival (ESOP, 2005)

Abstract interpretation of programs as Markov decision processes. - David Monniaux (Sci. Comput. Program., 2005)

Combination of Abstractions in the ASTRÉE Static Analyzer. - Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; David Monniaux; Xavier Rival (ASIAN, 2006)

Verification of device drivers and intelligent controllers: a case study. - David Monniaux (EMSOFT, 2007)

Optimal Abstraction on Real-Valued Programs. - David Monniaux (SAS, 2007)

Varieties of Static Analyzers: A Comparison with ASTREE. - Patrick Cousot; Radhia Cousot; Jérôme Feret; Antoine Miné; Laurent Mauborgne; David Monniaux; Xavier Rival (TASE, 2007)

Applying the Z-transform for the static analysis of floating-point numerical filters - David Monniaux (CoRR, 2007)

A Quantifier Elimination Algorithm for Linear Real Arithmetic. - David Monniaux (LPAR, 2008)

The pitfalls of verifying floating-point computations. - David Monniaux (ACM Trans. Program. Lang. Syst., 2008)

Analyse statique : de la théorie à la pratique ; analyse statique de code embarqué de grande taille, génération de domaines abstraits. (Static analysis: from theory to practice ; Static analysis of large-scale embedded code, generation of abstract domains). - David Monniaux (2009)

On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. - David Monniaux (CAV, 2009)

Automatic modular abstractions for linear constraints. - David Monniaux (POPL, 2009)

A minimalistic look at widening operators. - David Monniaux (High. Order Symb. Comput., 2009)

Quantifier Elimination by Lazy Model Enumeration. - David Monniaux (CAV, 2010)

Automatic Modular Abstractions for Template Numerical Constraints - David Monniaux (Log. Methods Comput. Sci., 2010)

Modular Abstractions of Reactive Nodes Using Disjunctive Invariants. - David Monniaux; Martin Bodin (APLAS, 2011)

Improving Strategies via SMT Solving. - Thomas Martin Gawlitza; David Monniaux (ESOP, 2011)

On the Generation of Positivstellensatz Witnesses in Degenerate Cases. - David Monniaux; Pierre Corbineau (ITP, 2011)

Using Bounded Model Checking to Focus Fixpoint Iterations. - David Monniaux; Laure Gonnord (SAS, 2011)

Stratified Static Analysis Based on Variable Dependencies. - David Monniaux; Julien Le Guen (NSAD@SAS, 2011)

Experiments on the feasibility of using a floating-point simplex in an SMT solver. - Diego Caminha Barbosa De Oliveira; David Monniaux (PAAR@IJCAR, 2012)

Anatomy of Alternating Quantifier Satisfiability (Work in progress). - Anh-Dung Phan; Nikolaj S. Bjørner; David Monniaux (SMT@IJCAR, 2012)

Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation. - Julien Henry; David Monniaux; Matthieu Moy (SAS, 2012)

Succinct Representations for Abstract Interpretation - Julien Henry; David Monniaux; Matthieu Moy (CoRR, 2012)

PAGAI: a path sensitive static analyzer - Julien Henry; David Monniaux; Matthieu Moy (CoRR, 2012)

Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs - Thomas Martin Gawlitza; David Monniaux (Log. Methods Comput. Sci., 2012)

PAGAI: A Path Sensitive Static Analyser. - Julien Henry; David Monniaux; Matthieu Moy (TAPAS@SAS, 2012)

Implementing Hash-Consed Structures in Coq. - Thomas Braibant; Jacques-Henri Jourdan; David Monniaux (ITP, 2013)

Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. - Alexis Fouilhé; David Monniaux; Michaël Périn (SAS, 2013)

How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. - Julien Henry; Mihail Asavoae; David Monniaux; Claire Maiza (LCTES, 2014)

Speeding Up Logico-Numerical Strategy Iteration. - David Monniaux; Peter Schrammel (SAS, 2014)

Scaling up logico-numerical strategy iteration (extended version). - David Monniaux; Peter Schrammel (CoRR, 2014)

Implementing and Reasoning About Hash-consed Data Structures in Coq. - Thomas Braibant; Jacques-Henri Jourdan; David Monniaux (J. Autom. Reason., 2014)

Synthesis of ranking functions using extremal counterexamples. - Laure Gonnord; David Monniaux; Gabriel Radanne (PLDI, 2015)

Polyhedra to the rescue of array interpolants. - Francesco Alberti; David Monniaux (SAC, 2015)

A Simple Abstraction of Arrays and Maps by Program Translation. - David Monniaux; Francesco Alberti (SAS, 2015)

An encoding of array verification problems into array-free Horn clauses. - David Monniaux; Laure Gonnord (CoRR, 2015)

A Survey of Satisfiability Modulo Theory. - David Monniaux (CASC, 2016)

Formula Slicing: Inductive Invariants from Preconditions. - Egor George Karpenkov; David Monniaux (Haifa Verification Conference, 2016)

Cell Morphing: From Array Programs to Array-Free Horn Clauses. - David Monniaux; Laure Gonnord (SAS, 2016)

Program Analysis with Local Policy Iteration. - Egor George Karpenkov; David Monniaux; Philipp Wendler (VMCAI, 2016)

Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem. - Alexandre Maréchal; Alexis Fouilhé; Tim King 001; David Monniaux; Michaël Périn (VMCAI, 2016)

Ascertaining Uncertainty for Efficient Exact Cache Analysis. - Valentin Touzeau; Claire Maïza; David Monniaux; Jan Reineke 001 (CAV (2), 2017)

Combining Forward and Backward Abstract Interpretation of Horn Clauses. - Alexey Bakhirkin; David Monniaux (SAS, 2017)

Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. - Alexandre Maréchal; David Monniaux; Michaël Périn (SAS, 2017)

Model Checking of Cache for WCET Analysis Refinement. - Valentin Touzeau; Claire Maïza; David Monniaux (CoRR, 2017)

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints. - Alexey Bakhirkin; David Monniaux (SAS, 2018)

The Verified Polyhedron Library: an Overview. - Sylvain Boulmé; Alexandre Maréchal; David Monniaux; Michaël Périn; Hang Yu 005 (SYNASC, 2018)

Parallel Parametric Linear Programming Solving, and Application to Polyhedral Computations. - Camille Coti; David Monniaux; Hang Yu 005 (ICCS (5), 2019)

An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection. - Hang Yu 005; David Monniaux (SAS, 2019)

On the decidability of the existence of polyhedral invariants in transition systems. - David Monniaux (Acta Informatica, 2019)

On the Complexity of Cache Analysis for Different Replacement Policies. - David Monniaux; Valentin Touzeau (J. ACM, 2019)

Fast and exact analysis for LRU caches. - Valentin Touzeau; Claire Maïza; David Monniaux; Jan Reineke 001 (Proc. ACM Program. Lang., 2019)

Certified and efficient instruction scheduling: application to interlocked VLIW processors. - Cyril Six; Sylvain Boulmé; David Monniaux (Proc. ACM Program. Lang., 2020)

Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. - David Monniaux; Cyril Six (LCTES, 2021)

Data Abstraction: A General Framework to Handle Program Verification of Data Structures. - Julien Braine; Laure Gonnord; David Monniaux (SAS, 2021)

A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations. - Camille Coti; David Monniaux; Hang Yu 005 (Concurr. Comput. Pract. Exp., 2021)

The complexity gap in the static analysis of cache accesses grows if procedure calls are added. - David Monniaux (Formal Methods Syst. Des., 2021)

Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic. - David Monniaux; Alice Pain (ARITH, 2022)

Formally verified superblock scheduling. - Cyril Six; Léo Gourdin; Sylvain Boulmé; David Monniaux; Justus Fasse; Nicolas Nardino (CPP, 2022)

The Trusted Computing Base of the CompCert Verified Compiler. - David Monniaux; Sylvain Boulmé (ESOP, 2022)

BaxMC: a CEGAR approach to Max#SAT. - Thomas Vigouroux; Cristian Ene; David Monniaux; Laurent Mounier; Marie-Laure Potet (FMCAD, 2022)

NP#P = ∃PP and other remarks about maximized counting. - David Monniaux (CoRR, 2022)

Completeness in static analysis by abstract interpretation, a personal point of view. - David Monniaux (CoRR, 2022)

Testing a Formally Verified Compiler. - David Monniaux; Léo Gourdin; Sylvain Boulmé; Olivier Lebeltel (TAP, 2023)

Formally Verified Loop-Invariant Code Motion and Assorted Optimizations. - David Monniaux; Cyril Six (ACM Trans. Embed. Comput. Syst., 2023)

Completeness in Static Analysis by Abstract Interpretation: A Personal Point of View. - David Monniaux (Challenges of Software Verification, 2023)

Formally Verifying Optimizations with Block Simulations. - Léo Gourdin; Benjamin Bonneau; Sylvain Boulmé; David Monniaux; Alexandre Bérard (Proc. ACM Program. Lang., 2023)

Memory Simulations, Security and Optimization in a Verified Compiler. - David Monniaux (CPP, 2024)

Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilers. - David Monniaux (Int. J. Softw. Tools Technol. Transf., 2024)

Formally Verified Hardening of C Programs against Hardware Fault Injection. - Basile Pesin; Sylvain Boulmé; David Monniaux; Marie-Laure Potet (CPP, 2025)