David Monniaux

According to our database, David Monniaux authored at least 80 papers between 1999 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Memory Simulations, Security and Optimization in a Verified Compiler.

David Monniaux

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Formally Verifying Optimizations with Block Simulations.

Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard

Proc. ACM Program. Lang., October, 2023

Formally Verified Loop-Invariant Code Motion and Assorted Optimizations.

David Monniaux, Cyril Six

ACM Trans. Embed. Comput. Syst., 2023

Testing a Formally Verified Compiler.

David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel

Proceedings of the Tests and Proofs - 17th International Conference, 2023

2022

Completeness in static analysis by abstract interpretation, a personal point of view.

David Monniaux

CoRR, 2022

NP^#P = ∃PP and other remarks about maximized counting.

David Monniaux

CoRR, 2022

BaxMC: a CEGAR approach to Max#SAT.

Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

The Trusted Computing Base of the CompCert Verified Compiler.

David Monniaux, Sylvain Boulmé

Proceedings of the Programming Languages and Systems, 2022

Formally verified superblock scheduling.

Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic.

David Monniaux, Alice Pain

Proceedings of the 29th IEEE Symposium on Computer Arithmetic, 2022

2021

The complexity gap in the static analysis of cache accesses grows if procedure calls are added.

David Monniaux

Formal Methods Syst. Des., 2021

A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations.

Camille Coti, David Monniaux, Hang Yu

Concurr. Comput. Pract. Exp., 2021

Data Abstraction: A General Framework to Handle Program Verification of Data Structures.

Julien Braine, Laure Gonnord, David Monniaux

Proceedings of the Static Analysis - 28th International Symposium, 2021

Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion.

David Monniaux, Cyril Six

Proceedings of the LCTES '21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, 2021

2020

Certified and efficient instruction scheduling: application to interlocked VLIW processors.

Cyril Six, Sylvain Boulmé, David Monniaux

Proc. ACM Program. Lang., 2020

2019

Fast and exact analysis for LRU caches.

Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke

Proc. ACM Program. Lang., 2019

On the Complexity of Cache Analysis for Different Replacement Policies.

David Monniaux, Valentin Touzeau

J. ACM, 2019

On the decidability of the existence of polyhedral invariants in transition systems.

David Monniaux

Acta Informatica, 2019

An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection.

Hang Yu, David Monniaux

Proceedings of the Static Analysis - 26th International Symposium, 2019

Parallel Parametric Linear Programming Solving, and Application to Polyhedral Computations.

Camille Coti, David Monniaux, Hang Yu

Proceedings of the Computational Science - ICCS 2019, 2019

2018

The Verified Polyhedron Library: an Overview.

Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu

Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints.

Alexey Bakhirkin, David Monniaux

Proceedings of the Static Analysis - 25th International Symposium, 2018

2017

Model Checking of Cache for WCET Analysis Refinement.

Valentin Touzeau, Claire Maïza, David Monniaux

CoRR, 2017

Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming.

Alexandre Maréchal, David Monniaux, Michaël Périn

Proceedings of the Static Analysis - 24th International Symposium, 2017

Combining Forward and Backward Abstract Interpretation of Horn Clauses.

Alexey Bakhirkin, David Monniaux

Proceedings of the Static Analysis - 24th International Symposium, 2017

Ascertaining Uncertainty for Efficient Exact Cache Analysis.

Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem.

Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Program Analysis with Local Policy Iteration.

Egor George Karpenkov, David Monniaux, Philipp Wendler

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Cell Morphing: From Array Programs to Array-Free Horn Clauses.

David Monniaux, Laure Gonnord

Proceedings of the Static Analysis - 23rd International Symposium, 2016

Formula Slicing: Inductive Invariants from Preconditions.

Egor George Karpenkov, David Monniaux

Proceedings of the Hardware and Software: Verification and Testing, 2016

A Survey of Satisfiability Modulo Theory.

David Monniaux

Proceedings of the Computer Algebra in Scientific Computing - 18th International Workshop, 2016

2015

An encoding of array verification problems into array-free Horn clauses.

David Monniaux, Laure Gonnord

CoRR, 2015

A Simple Abstraction of Arrays and Maps by Program Translation.

David Monniaux, Francesco Alberti

Proceedings of the Static Analysis - 22nd International Symposium, 2015

Polyhedra to the rescue of array interpolants.

Francesco Alberti, David Monniaux

Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Synthesis of ranking functions using extremal counterexamples.

Laure Gonnord, David Monniaux, Gabriel Radanne

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2014

Implementing and Reasoning About Hash-consed Data Structures in Coq.

Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

J. Autom. Reason., 2014

Scaling up logico-numerical strategy iteration (extended version).

David Monniaux, Peter Schrammel

CoRR, 2014

Speeding Up Logico-Numerical Strategy Iteration.

David Monniaux, Peter Schrammel

Proceedings of the Static Analysis - 21st International Symposium, 2014

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

Proceedings of the SIGPLAN/SIGBED Conference on Languages, 2014

2013

Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra.

Alexis Fouilhé, David Monniaux, Michaël Périn

Proceedings of the Static Analysis - 20th International Symposium, 2013

Implementing Hash-Consed Structures in Coq.

Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

PAGAI: A Path Sensitive Static Analyser.

Julien Henry, David Monniaux, Matthieu Moy

Proceedings of the Third Workshop on Tools for Automatic Program Analysis, 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 analyzer

Julien Henry, David Monniaux, Matthieu Moy

CoRR, 2012

Succinct Representations for Abstract Interpretation

Julien Henry, David Monniaux, Matthieu Moy

CoRR, 2012

Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation.

Julien Henry, David Monniaux, Matthieu Moy

Proceedings of the Static Analysis - 19th International Symposium, 2012

Anatomy of Alternating Quantifier Satisfiability (Work in progress).

Anh-Dung Phan, Nikolaj S. Bjørner, David Monniaux

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Experiments on the feasibility of using a floating-point simplex in an SMT solver.

Diego Caminha Barbosa De Oliveira, David Monniaux

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011

Stratified Static Analysis Based on Variable Dependencies.

David Monniaux, Julien Le Guen

Proceedings of the Third International Workshop on Numerical and Symbolic Abstract Domains, 2011

Using Bounded Model Checking to Focus Fixpoint Iterations.

David Monniaux, Laure Gonnord

Proceedings of the Static Analysis - 18th International Symposium, 2011

On the Generation of Positivstellensatz Witnesses in Degenerate Cases.

David Monniaux, Pierre Corbineau

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Improving Strategies via SMT Solving.

Thomas Martin Gawlitza, David Monniaux

Proceedings of the Programming Languages and Systems, 2011

Modular Abstractions of Reactive Nodes Using Disjunctive Invariants.

David Monniaux, Martin Bodin

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010

Automatic Modular Abstractions for Template Numerical Constraints

David Monniaux

Log. Methods Comput. Sci., 2010

Quantifier Elimination by Lazy Model Enumeration.

David Monniaux

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

A minimalistic look at widening operators.

David Monniaux

High. Order Symb. Comput., 2009

Automatic modular abstractions for linear constraints.

David Monniaux

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure.

David Monniaux

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

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

2008

The pitfalls of verifying floating-point computations.

David Monniaux

ACM Trans. Program. Lang. Syst., 2008

A Quantifier Elimination Algorithm for Linear Real Arithmetic.

David Monniaux

Proceedings of the Logic for Programming, 2008

2007

Applying the Z-transform for the static analysis of floating-point numerical filters

David Monniaux

CoRR, 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

Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

Optimal Abstraction on Real-Valued Programs.

David Monniaux

Proceedings of the Static Analysis, 14th International Symposium, 2007

Verification of device drivers and intelligent controllers: a case study.

David Monniaux

Proceedings of the 7th ACM & IEEE International conference on Embedded software, 2007

2006

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

Proceedings of the Advances in Computer Science, 2006

2005

Abstract interpretation of programs as Markov decision processes.

David Monniaux

Sci. Comput. Program., 2005

The ASTREÉ Analyzer.

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival

Proceedings of the Programming Languages and Systems, 2005

Compositional Analysis of Floating-Point Linear Numerical Filters.

David Monniaux

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The Parallel Implementation of the Astrée Static Analyzer.

David Monniaux

Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2003

Abstracting cryptographic protocols with tree automata.

David Monniaux

Sci. Comput. Program., 2003

Abstraction of Expectation Functions Using Gaussian Distributions.

David Monniaux

Proceedings of the Verification, 2003

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

Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

2002

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

Proceedings of the Essence of Computation, Complexity, Analysis, 2002

2001

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

David Monniaux

PhD thesis, 2001

An Abstract Analysis of the Probabilistic Termination of Programs.

David Monniaux

Proceedings of the Static Analysis, 8th International Symposium, 2001

An abstract Monte-Carlo method for the analysis of probabilistic programs.

David Monniaux

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

Backwards Abstract Interpretation of Probabilistic Programs.

David Monniaux

Proceedings of the Programming Languages and Systems, 2001

2000

Abstract Interpretation of Probabilistic Semantics.

David Monniaux

Proceedings of the Static Analysis, 7th International Symposium, 2000

1999

Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief.

David Monniaux

Proceedings of the 12th IEEE Computer Security Foundations Workshop, 1999