David Monniaux

ORCID

Publication Activity (10 Years)

Years Active: 1999-2024
Publications (10 Years): 53

Top Venues

CoRR

SAS

Proc. ACM Program. Lang.

VMCAI

Paris Dauphine University, France (PHD)

Education History

Paris Dauphine University, France

PHD

Publications

David Monniaux
Memory Simulations, Security and Optimization in a Verified Compiler. CPP (2024)
David Monniaux
Memory Simulations, Security and Optimization in a Verified Compiler. CoRR (2023)
David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel
Testing a Formally Verified Compiler. TAP (2023)
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard
Formally Verifying Optimizations with Block Simulations. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
David Monniaux, Cyril Six
Formally Verified Loop-Invariant Code Motion and Assorted Optimizations. ACM Trans. Embed. Comput. Syst. 22 (1) (2023)
Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet
BaxMC: a CEGAR approach to Max#SAT. FMCAD (2022)
Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet
BAXMC: a CEGAR approach to Max\#SAT. CoRR (2022)
David Monniaux, Sylvain Boulmé
The Trusted Computing Base of the CompCert Verified Compiler. CoRR (2022)
David Monniaux
The complexity gap in the static analysis of cache accesses grows if procedure calls are added. CoRR (2022)
David Monniaux
Completeness in static analysis by abstract interpretation, a personal point of view. CoRR (2022)
David Monniaux, Sylvain Boulmé
The Trusted Computing Base of the CompCert Verified Compiler. ESOP (2022)
David Monniaux, Alice Pain
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic. ARITH (2022)
David Monniaux
= ∃PP and other remarks about maximized counting. CoRR (2022)
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
Formally verified superblock scheduling. CPP (2022)
David Monniaux, Alice Pain
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic. CoRR (2022)
David Monniaux
The complexity gap in the static analysis of cache accesses grows if procedure calls are added. Formal Methods Syst. Des. 59 (1) (2021)
Camille Coti, David Monniaux, Hang Yu
A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations. Concurr. Comput. Pract. Exp. 33 (6) (2021)
Julien Braine, Laure Gonnord, David Monniaux
Data Abstraction: A General Framework to Handle Program Verification of Data Structures. SAS (2021)
David Monniaux, Cyril Six
Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion. CoRR (2021)
David Monniaux, Cyril Six
Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. LCTES (2021)
Cyril Six, Sylvain Boulmé, David Monniaux
Certified and efficient instruction scheduling: application to interlocked VLIW processors. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Camille Coti, David Monniaux, Hang Yu
A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations. CoRR (2020)
Camille Coti, David Monniaux, Hang Yu
Parallel parametric linear programming solving, and application to polyhedral computations. CoRR (2019)
Camille Coti, David Monniaux, Hang Yu
Parallel Parametric Linear Programming Solving, and Application to Polyhedral Computations. ICCS (5) (2019)
Hang Yu, David Monniaux
An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection. SAS (2019)
David Monniaux, Valentin Touzeau
On the Complexity of Cache Analysis for Different Replacement Policies. J. ACM 66 (6) (2019)
Hang Yu, David Monniaux
An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection. CoRR (2019)
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
Fast and exact analysis for LRU caches. Proc. ACM Program. Lang. 3 (POPL) (2019)
David Monniaux
On the decidability of the existence of polyhedral invariants in transition systems. Acta Informatica 56 (4) (2019)
David Monniaux, Valentin Touzeau
On the complexity of cache analysis for different replacement policies. CoRR (2018)
Alexey Bakhirkin, David Monniaux
Extending Constraint-Only Representation of Polyhedra with Boolean Constraints. SAS (2018)
Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu
The Verified Polyhedron Library: an Overview. SYNASC (2018)
Claire Maïza, Valentin Touzeau, David Monniaux, Jan Reineke
Fast and exact analysis for LRU caches. CoRR (2018)
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
Ascertaining Uncertainty for Efficient Exact Cache Analysis. CoRR (2017)
Alexey Bakhirkin, David Monniaux
Combining Forward and Backward Abstract Interpretation of Horn Clauses. CoRR (2017)
Valentin Touzeau, Claire Maïza, David Monniaux
Model Checking of Cache for WCET Analysis Refinement. CoRR (2017)
David Monniaux
On the decidability of the existence of polyhedral invariants in transition systems. CoRR (2017)
Alexey Bakhirkin, David Monniaux
Combining Forward and Backward Abstract Interpretation of Horn Clauses. SAS (2017)
Alexandre Maréchal, David Monniaux, Michaël Périn
Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. SAS (2017)
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
Ascertaining Uncertainty for Efficient Exact Cache Analysis. CAV (2) (2017)
Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn
Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem. VMCAI (2016)
Egor George Karpenkov, David Monniaux, Philipp Wendler
Program Analysis with Local Policy Iteration. VMCAI (2016)
David Monniaux
A Survey of Satisfiability Modulo Theory. CoRR (2016)
David Monniaux, Laure Gonnord
Cell Morphing: From Array Programs to Array-Free Horn Clauses. SAS (2016)
Egor George Karpenkov, David Monniaux
Formula Slicing: Inductive Invariants from Preconditions. Haifa Verification Conference (2016)
David Monniaux
A Survey of Satisfiability Modulo Theory. CASC (2016)
Egor George Karpenkov, David Monniaux
Formula Slicing: Inductive Invariants from Preconditions. CoRR (2016)
Francesco Alberti, David Monniaux
Polyhedra to the rescue of array interpolants. SAC (2015)
David Monniaux, Francesco Alberti
A Simple Abstraction of Arrays and Maps by Program Translation. SAS (2015)
George Karpenkov, David Monniaux, Philipp Wendler
Program Analysis with Local Policy Iteration. CoRR (2015)
David Monniaux, Laure Gonnord
An encoding of array verification problems into array-free Horn clauses. CoRR (2015)
David Monniaux, Francesco Alberti
A simple abstraction of arrays and maps by program translation. CoRR (2015)
Laure Gonnord, David Monniaux, Gabriel Radanne
Synthesis of ranking functions using extremal counterexamples. PLDI (2015)
David Monniaux, Peter Schrammel
Scaling up logico-numerical strategy iteration (extended version). CoRR (2014)
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
Implementing and Reasoning About Hash-consed Data Structures in Coq. J. Autom. Reason. 53 (3) (2014)
Julien Henry, Mihail Asavoae, David Monniaux, Claire Maiza
How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. LCTES (2014)
David Monniaux, Peter Schrammel
Speeding Up Logico-Numerical Strategy Iteration. SAS (2014)
Julien Henry, Mihail Asavoae, David Monniaux, Claire Maïza
How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics. CoRR (2014)
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
Implementing Hash-Consed Structures in Coq. ITP (2013)
Alexis Fouilhé, David Monniaux, Michaël Périn
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra CoRR (2013)
Alexis Fouilhé, David Monniaux, Michaël Périn
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. SAS (2013)
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
Implementing and reasoning about hash-consed data structures in Coq. CoRR (2013)
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
Implementing hash-consed structures in Coq CoRR (2013)
Diego Caminha Barbosa De Oliveira, David Monniaux
Experiments on the feasibility of using a floating-point simplex in an SMT solver. PAAR@IJCAR (2012)
Julien Henry, David Monniaux, Matthieu Moy
Succinct Representations for Abstract Interpretation CoRR (2012)
Anh-Dung Phan, Nikolaj Bjørner, David Monniaux
Anatomy of Alternating Quantifier Satisfiability (Work in progress). SMT@IJCAR (2012)
Julien Henry, David Monniaux, Matthieu Moy
Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation. SAS (2012)
Julien Henry, David Monniaux, Matthieu Moy
PAGAI: a path sensitive static analyzer CoRR (2012)
Thomas Martin Gawlitza, David Monniaux
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs Log. Methods Comput. Sci. 8 (3) (2012)
David Monniaux, Julien Le Guen
Stratified Static Analysis Based on Variable Dependencies. Electron. Notes Theor. Comput. Sci. 288 (2012)
Julien Henry, David Monniaux, Matthieu Moy
PAGAI: A Path Sensitive Static Analyser. Electron. Notes Theor. Comput. Sci. 289 (2012)
David Monniaux, Martin Bodin
Modular Abstractions of Reactive Nodes using Disjunctive Invariants CoRR (2011)
David Monniaux, Martin Bodin
Modular Abstractions of Reactive Nodes Using Disjunctive Invariants. APLAS (2011)
David Monniaux, Pierre Corbineau
On the Generation of Positivstellensatz Witnesses in Degenerate Cases. ITP (2011)
Thomas Martin Gawlitza, David Monniaux
Improving Strategies via SMT Solving CoRR (2011)
David Monniaux, Laure Gonnord
Using Bounded Model Checking to Focus Fixpoint Iterations. SAS (2011)
David Monniaux, Pierre Corbineau
On the Generation of Positivstellensatz Witnesses in Degenerate Cases CoRR (2011)
David Monniaux, Laure Gonnord
Using Bounded Model Checking to Focus Fixpoint Iterations CoRR (2011)
Thomas Martin Gawlitza, David Monniaux
Improving Strategies via SMT Solving. ESOP (2011)
David Monniaux, Julien Le Guen
Stratified Static Analysis Based on Variable Dependencies CoRR (2011)
David Monniaux
Quantifier Elimination by Lazy Model Enumeration. CAV (2010)
David Monniaux
Automatic Modular Abstractions for Template Numerical Constraints Log. Methods Comput. Sci. 6 (3) (2010)
David Monniaux
Automatic modular abstractions for template numerical constraints CoRR (2009)
David Monniaux
A minimalistic look at widening operators CoRR (2009)
David Monniaux
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. CAV (2009)
David Monniaux
Automatic modular abstractions for linear constraints. POPL (2009)
David Monniaux
A minimalistic look at widening operators. High. Order Symb. Comput. 22 (2) (2009)
David Monniaux
On using floating-point computations to help an exact linear arithmetic decision procedure CoRR (2009)
David Monniaux
A Quantifier Elimination Algorithm for Linear Real Arithmetic. LPAR (2008)
David Monniaux
The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. 30 (3) (2008)
David Monniaux
A Quantifier Elimination Algorithm for Linear Real Arithmetic CoRR (2008)
David Monniaux
Automatic Modular Abstractions for Linear Constraints CoRR (2008)
David Monniaux
The parallel implementation of the Astrée static analyzer CoRR (2007)
David Monniaux
Optimal Abstraction on Real-Valued Programs. SAS (2007)
David Monniaux
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs CoRR (2007)
David Monniaux
The pitfalls of verifying floating-point computations CoRR (2007)
David Monniaux
Verification of device drivers and intelligent controllers: a case study. EMSOFT (2007)
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
A Static Analyzer for Large Safety-Critical Software CoRR (2007)
Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Laurent Mauborgne, David Monniaux, Xavier Rival
Varieties of Static Analyzers: A Comparison with ASTREE. TASE (2007)
David Monniaux
Applying the Z-transform for the static analysis of floating-point numerical filters CoRR (2007)

David Monniaux.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

David Monniaux