David Monniaux

125 papers A* 7A 4B 32C 2Misc 4Journal 61Unranked 11
YearRankTypeTitle / Venue / Authors
2026 — conf
Max-Policy Iteration, Revisited.
ESOP (2)
David Monniaux, Helmut Seidl
2025 B conf
Formally Verified Hardening of C Programs against Hardware Fault Injection.
CPP
Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet
2024 B conf
Memory Simulations, Security and Optimization in a Verified Compiler.
CPP
David Monniaux
2024 J jnl
Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers.
CoRR
David Monniaux
2024 J jnl
Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilers.
Int. J. Softw. Tools Technol. Transf.
David Monniaux
2024 — ed.
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis, LSFA/HCVS 2023, and 10th Workshop on Horn Clauses for Verification and Synthesis, Rome, Italy & Paris, France, July 1-2, 2023 & April 23, 2023.
LSFA/HCVS
Temur Kutsia, Daniel Ventura, David Monniaux, José F. Morales
2023 — ch.
Completeness in Static Analysis by Abstract Interpretation: A Personal Point of View.
Challenges of Software Verification
David Monniaux
2023 J jnl
Formally Verified Loop-Invariant Code Motion and Assorted Optimizations.
ACM Trans. Embed. Comput. Syst.
David Monniaux, Cyril Six
2023 J jnl
Formally Verifying Optimizations with Block Simulations.
Proc. ACM Program. Lang.
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard
2023 J jnl
Memory Simulations, Security and Optimization in a Verified Compiler.
CoRR
David Monniaux
2023 C conf
Testing a Formally Verified Compiler.
TAP
David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel
2022 J jnl
BAXMC: a CEGAR approach to Max\#SAT.
CoRR
Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet
2022 B conf
BaxMC: a CEGAR approach to Max#SAT.
FMCAD
Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet
2022 J jnl
Completeness in static analysis by abstract interpretation, a personal point of view.
CoRR
David Monniaux
2022 C conf
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic.
ARITH
David Monniaux, Alice Pain
2022 J jnl
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic.
CoRR
David Monniaux, Alice Pain
2022 B conf
Formally verified superblock scheduling.
CPP
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
2022 J jnl
NP
CoRR
David Monniaux
2022 A conf
The Trusted Computing Base of the CompCert Verified Compiler.
ESOP
David Monniaux, Sylvain Boulmé
2022 J jnl
The Trusted Computing Base of the CompCert Verified Compiler.
CoRR
David Monniaux, Sylvain Boulmé
2022 J jnl
The complexity gap in the static analysis of cache accesses grows if procedure calls are added.
CoRR
David Monniaux
2021 J jnl
A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations.
Concurr. Comput. Pract. Exp.
Camille Coti, David Monniaux, Hang Yu
2021 B conf
Data Abstraction: A General Framework to Handle Program Verification of Data Structures.
SAS
Julien Braine, Laure Gonnord, David Monniaux
2021 J jnl
Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion.
CoRR
David Monniaux, Cyril Six
2021 B conf
Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion.
LCTES
David Monniaux, Cyril Six
2021 J jnl
The complexity gap in the static analysis of cache accesses grows if procedure calls are added.
Formal Methods Syst. Des.
David Monniaux
2020 J jnl
A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations.
CoRR
Camille Coti, David Monniaux, Hang Yu
2020 J jnl
Certified and efficient instruction scheduling: application to interlocked VLIW processors.
Proc. ACM Program. Lang.
Cyril Six, Sylvain Boulmé, David Monniaux
2019 B conf
An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection.
SAS
Hang Yu, David Monniaux
2019 J jnl
An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection.
CoRR
Hang Yu, David Monniaux
2019 J jnl
Fast and exact analysis for LRU caches.
Proc. ACM Program. Lang.
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
2019 J jnl
On the Complexity of Cache Analysis for Different Replacement Policies.
J. ACM
David Monniaux, Valentin Touzeau
2019 J jnl
On the decidability of the existence of polyhedral invariants in transition systems.
Acta Informatica
David Monniaux
2019 — conf
Parallel Parametric Linear Programming Solving, and Application to Polyhedral Computations.
ICCS (5)
Camille Coti, David Monniaux, Hang Yu
2019 J jnl
Parallel parametric linear programming solving, and application to polyhedral computations.
CoRR
Camille Coti, David Monniaux, Hang Yu
2018 B conf
Extending Constraint-Only Representation of Polyhedra with Boolean Constraints.
SAS
Alexey Bakhirkin, David Monniaux
2018 J jnl
Fast and exact analysis for LRU caches.
CoRR
Claire Maïza, Valentin Touzeau, David Monniaux, Jan Reineke
2018 J jnl
On the complexity of cache analysis for different replacement policies.
CoRR
David Monniaux, Valentin Touzeau
2018 Misc conf
The Verified Polyhedron Library: an Overview.
SYNASC
Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu
2017 — conf
Ascertaining Uncertainty for Efficient Exact Cache Analysis.
CAV (2)
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
2017 J jnl
Ascertaining Uncertainty for Efficient Exact Cache Analysis.
CoRR
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
2017 B conf
Combining Forward and Backward Abstract Interpretation of Horn Clauses.
SAS
Alexey Bakhirkin, David Monniaux
2017 J jnl
Combining Forward and Backward Abstract Interpretation of Horn Clauses.
CoRR
Alexey Bakhirkin, David Monniaux
2017 J jnl
Model Checking of Cache for WCET Analysis Refinement.
CoRR
Valentin Touzeau, Claire Maïza, David Monniaux
2017 J jnl
On the decidability of the existence of polyhedral invariants in transition systems.
CoRR
David Monniaux
2017 B conf
Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming.
SAS
Alexandre Maréchal, David Monniaux, Michaël Périn
2017 B ed.
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings
VNCAI
Ahmed Bouajjani, David Monniaux
2016 B conf
A Survey of Satisfiability Modulo Theory.
CASC
David Monniaux
2016 J jnl
A Survey of Satisfiability Modulo Theory.
CoRR
David Monniaux
2016 B conf
Cell Morphing: From Array Programs to Array-Free Horn Clauses.
SAS
David Monniaux, Laure Gonnord
2016 — conf
Formula Slicing: Inductive Invariants from Preconditions.
Haifa Verification Conference
Egor George Karpenkov, David Monniaux
2016 J jnl
Formula Slicing: Inductive Invariants from Preconditions.
CoRR
Egor George Karpenkov, David Monniaux
2016 B conf
Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem.
VMCAI
Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn
2016 B conf
Program Analysis with Local Policy Iteration.
VMCAI
Egor George Karpenkov, David Monniaux, Philipp Wendler
2015 B conf
A Simple Abstraction of Arrays and Maps by Program Translation.
SAS
David Monniaux, Francesco Alberti
2015 J jnl
A simple abstraction of arrays and maps by program translation.
CoRR
David Monniaux, Francesco Alberti
2015 J jnl
An encoding of array verification problems into array-free Horn clauses.
CoRR
David Monniaux, Laure Gonnord
2015 Misc conf
Polyhedra to the rescue of array interpolants.
SAC
Francesco Alberti, David Monniaux
2015 J jnl
Program Analysis with Local Policy Iteration.
CoRR
George Karpenkov, David Monniaux, Philipp Wendler
2015 A* conf
Synthesis of ranking functions using extremal counterexamples.
PLDI
Laure Gonnord, David Monniaux, Gabriel Radanne
2014 J jnl
How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics.
CoRR
Julien Henry, Mihail Asavoae, David Monniaux, Claire Maïza
2014 B conf
How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics.
LCTES
Julien Henry, Mihail Asavoae, David Monniaux, Claire Maiza
2014 J jnl
Implementing and Reasoning About Hash-consed Data Structures in Coq.
J. Autom. Reason.
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2014 J jnl
Scaling up logico-numerical strategy iteration (extended version).
CoRR
David Monniaux, Peter Schrammel
2014 B conf
Speeding Up Logico-Numerical Strategy Iteration.
SAS
David Monniaux, Peter Schrammel
2013 J jnl
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
CoRR
Alexis Fouilhé, David Monniaux, Michaël Périn
2013 B conf
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra.
SAS
Alexis Fouilhé, David Monniaux, Michaël Périn
2013 B conf
Implementing Hash-Consed Structures in Coq.
ITP
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Implementing and reasoning about hash-consed data structures in Coq.
CoRR
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Implementing hash-consed structures in Coq
CoRR
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2012 — conf
Anatomy of Alternating Quantifier Satisfiability (Work in progress).
SMT@IJCAR
Anh-Dung Phan, Nikolaj S. Bjørner, David Monniaux
2012 — conf
Experiments on the feasibility of using a floating-point simplex in an SMT solver.
PAAR@IJCAR
Diego Caminha Barbosa De Oliveira, David Monniaux
2012 J jnl
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
Log. Methods Comput. Sci.
Thomas Martin Gawlitza, David Monniaux
2012 — conf
PAGAI: A Path Sensitive Static Analyser.
TAPAS@SAS
Julien Henry, David Monniaux, Matthieu Moy
2012 J jnl
PAGAI: a path sensitive static analyzer
CoRR
Julien Henry, David Monniaux, Matthieu Moy
2012 J jnl
Succinct Representations for Abstract Interpretation
CoRR
Julien Henry, David Monniaux, Matthieu Moy
2012 B conf
Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation.
SAS
Julien Henry, David Monniaux, Matthieu Moy
2011 J jnl
Improving Strategies via SMT Solving
CoRR
Thomas Martin Gawlitza, David Monniaux
2011 A conf
Improving Strategies via SMT Solving.
ESOP
Thomas Martin Gawlitza, David Monniaux
2011 B conf
Modular Abstractions of Reactive Nodes Using Disjunctive Invariants.
APLAS
David Monniaux, Martin Bodin
2011 J jnl
Modular Abstractions of Reactive Nodes using Disjunctive Invariants
CoRR
David Monniaux, Martin Bodin
2011 J jnl
On the Generation of Positivstellensatz Witnesses in Degenerate Cases
CoRR
David Monniaux, Pierre Corbineau
2011 B conf
On the Generation of Positivstellensatz Witnesses in Degenerate Cases.
ITP
David Monniaux, Pierre Corbineau
2011 J jnl
Stratified Static Analysis Based on Variable Dependencies
CoRR
David Monniaux, Julien Le Guen
2011 — conf
Stratified Static Analysis Based on Variable Dependencies.
NSAD@SAS
David Monniaux, Julien Le Guen
2011 J jnl
Using Bounded Model Checking to Focus Fixpoint Iterations
CoRR
David Monniaux, Laure Gonnord
2011 B conf
Using Bounded Model Checking to Focus Fixpoint Iterations.
SAS
David Monniaux, Laure Gonnord
2010 J jnl
Automatic Modular Abstractions for Template Numerical Constraints
Log. Methods Comput. Sci.
David Monniaux
2010 A* conf
Quantifier Elimination by Lazy Model Enumeration.
CAV
David Monniaux
2009 J jnl
A minimalistic look at widening operators
CoRR
David Monniaux
2009 J jnl
A minimalistic look at widening operators.
High. Order Symb. Comput.
David Monniaux
2009 — book
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 A* conf
Automatic modular abstractions for linear constraints.
POPL
David Monniaux
2009 J jnl
Automatic modular abstractions for template numerical constraints
CoRR
David Monniaux
2009 A* conf
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure.
CAV
David Monniaux
2009 J jnl
On using floating-point computations to help an exact linear arithmetic decision procedure
CoRR
David Monniaux
2008 J jnl
A Quantifier Elimination Algorithm for Linear Real Arithmetic
CoRR
David Monniaux
2008 B conf
A Quantifier Elimination Algorithm for Linear Real Arithmetic.
LPAR
David Monniaux
2008 J jnl
Automatic Modular Abstractions for Linear Constraints
CoRR
David Monniaux
2008 J jnl
The pitfalls of verifying floating-point computations.
ACM Trans. Program. Lang. Syst.
David Monniaux
2007 J jnl
A Static Analyzer for Large Safety-Critical Software
CoRR
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2007 J jnl
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
CoRR
David Monniaux
2007 J jnl
Applying the Z-transform for the static analysis of floating-point numerical filters
CoRR
David Monniaux
2007 B conf
Optimal Abstraction on Real-Valued Programs.
SAS
David Monniaux
2007 J jnl
The parallel implementation of the Astrée static analyzer
CoRR
David Monniaux
2007 J jnl
The pitfalls of verifying floating-point computations
CoRR
David Monniaux
2007 Misc conf
Varieties of Static Analyzers: A Comparison with ASTREE.
TASE
Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Laurent Mauborgne, David Monniaux, Xavier Rival
2007 Misc conf
Verification of device drivers and intelligent controllers: a case study.
EMSOFT
David Monniaux
2006 — conf
Combination of Abstractions in the ASTRÉE Static Analyzer.
ASIAN
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2005 J jnl
Abstract interpretation of programs as Markov decision processes.
Sci. Comput. Program.
David Monniaux
2005 A* conf
Compositional Analysis of Floating-Point Linear Numerical Filters.
CAV
David Monniaux
2005 A conf
The ASTREÉ Analyzer.
ESOP
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2005 B conf
The Parallel Implementation of the Astrée Static Analyzer.
APLAS
David Monniaux
2003 A* conf
A static analyzer for large safety-critical software.
PLDI
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2003 B conf
Abstract Interpretation of Programs as Markov Decision Processes.
SAS
David Monniaux
2003 J jnl
Abstracting cryptographic protocols with tree automata.
Sci. Comput. Program.
David Monniaux
2003 B conf
Abstraction of Expectation Functions Using Gaussian Distributions.
VMCAI
David Monniaux
2002 — conf
Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software.
The Essence of Computation
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2001 B conf
An Abstract Analysis of the Probabilistic Termination of Programs.
SAS
David Monniaux
2001 A* conf
An abstract Monte-Carlo method for the analysis of probabilistic programs.
POPL
David Monniaux
2001 — —
Analysis of probabilistic programs by abstract interpretation. (Analyse de programmes probabilistes par interprétation abstraite).
David Monniaux
2001 A conf
Backwards Abstract Interpretation of Probabilistic Programs.
ESOP
David Monniaux
2000 B conf
Abstract Interpretation of Probabilistic Semantics.
SAS
David Monniaux
1999 B conf
Abstracting Cryptographic Protocols with Tree Automata.
SAS
David Monniaux
1999 — conf
Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief.
CSFW
David Monniaux