David Monniaux

Orcid: 0000-0001-7671-6126

Affiliations:
  • University of Grenoble, VERIMAG, France
  • Joseph Fourier University, Grenoble, France
  • Paris Dauphine University, France (PhD 2001)


According to our database1, David Monniaux authored at least 81 papers between 1999 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilers.
Int. J. Softw. Tools Technol. Transf., August, 2024

Memory Simulations, Security and Optimization in a Verified Compiler.
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023
Formally Verifying Optimizations with Block Simulations.
Proc. ACM Program. Lang., October, 2023

Formally Verified Loop-Invariant Code Motion and Assorted Optimizations.
ACM Trans. Embed. Comput. Syst., 2023

Testing a Formally Verified Compiler.
Proceedings of the Tests and Proofs - 17th International Conference, 2023

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

NP<sup>#P</sup> = ∃PP and other remarks about maximized counting.
CoRR, 2022

BaxMC: a CEGAR approach to Max#SAT.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

The Trusted Computing Base of the CompCert Verified Compiler.
Proceedings of the Programming Languages and Systems, 2022

Formally verified superblock scheduling.
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.
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.
Formal Methods Syst. Des., 2021

A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations.
Concurr. Comput. Pract. Exp., 2021

Data Abstraction: A General Framework to Handle Program Verification of Data Structures.
Proceedings of the Static Analysis - 28th International Symposium, 2021

Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion.
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.
Proc. ACM Program. Lang., 2020

2019
Fast and exact analysis for LRU caches.
Proc. ACM Program. Lang., 2019

On the Complexity of Cache Analysis for Different Replacement Policies.
J. ACM, 2019

On the decidability of the existence of polyhedral invariants in transition systems.
Acta Informatica, 2019

An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection.
Proceedings of the Static Analysis - 26th International Symposium, 2019

Parallel Parametric Linear Programming Solving, and Application to Polyhedral Computations.
Proceedings of the Computational Science - ICCS 2019, 2019

2018
The Verified Polyhedron Library: an Overview.
Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

Extending Constraint-Only Representation of Polyhedra with Boolean Constraints.
Proceedings of the Static Analysis - 25th International Symposium, 2018

2017
Model Checking of Cache for WCET Analysis Refinement.
CoRR, 2017

Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming.
Proceedings of the Static Analysis - 24th International Symposium, 2017

Combining Forward and Backward Abstract Interpretation of Horn Clauses.
Proceedings of the Static Analysis - 24th International Symposium, 2017

Ascertaining Uncertainty for Efficient Exact Cache Analysis.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Program Analysis with Local Policy Iteration.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Cell Morphing: From Array Programs to Array-Free Horn Clauses.
Proceedings of the Static Analysis - 23rd International Symposium, 2016

Formula Slicing: Inductive Invariants from Preconditions.
Proceedings of the Hardware and Software: Verification and Testing, 2016

A Survey of Satisfiability Modulo Theory.
Proceedings of the Computer Algebra in Scientific Computing - 18th International Workshop, 2016

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

A Simple Abstraction of Arrays and Maps by Program Translation.
Proceedings of the Static Analysis - 22nd International Symposium, 2015

Polyhedra to the rescue of array interpolants.
Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Synthesis of ranking functions using extremal counterexamples.
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.
J. Autom. Reason., 2014

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

Speeding Up Logico-Numerical Strategy Iteration.
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.
Proceedings of the SIGPLAN/SIGBED Conference on Languages, 2014

2013
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Implementing Hash-Consed Structures in Coq.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012
PAGAI: A Path Sensitive Static Analyser.
Proceedings of the Third Workshop on Tools for Automatic Program Analysis, 2012

Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
Log. Methods Comput. Sci., 2012

PAGAI: a path sensitive static analyzer
CoRR, 2012

Succinct Representations for Abstract Interpretation
CoRR, 2012

Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Anatomy of Alternating Quantifier Satisfiability (Work in progress).
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.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011
Stratified Static Analysis Based on Variable Dependencies.
Proceedings of the Third International Workshop on Numerical and Symbolic Abstract Domains, 2011

Using Bounded Model Checking to Focus Fixpoint Iterations.
Proceedings of the Static Analysis - 18th International Symposium, 2011

On the Generation of Positivstellensatz Witnesses in Degenerate Cases.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Improving Strategies via SMT Solving.
Proceedings of the Programming Languages and Systems, 2011

Modular Abstractions of Reactive Nodes Using Disjunctive Invariants.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010
Automatic Modular Abstractions for Template Numerical Constraints
Log. Methods Comput. Sci., 2010

Quantifier Elimination by Lazy Model Enumeration.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
A minimalistic look at widening operators.
High. Order Symb. Comput., 2009

Automatic modular abstractions for linear constraints.
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.
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).
, 2009

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

A Quantifier Elimination Algorithm for Linear Real Arithmetic.
Proceedings of the Logic for Programming, 2008

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

Varieties of Static Analyzers: A Comparison with ASTREE.
Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

Optimal Abstraction on Real-Valued Programs.
Proceedings of the Static Analysis, 14th International Symposium, 2007

Verification of device drivers and intelligent controllers: a case study.
Proceedings of the 7th ACM & IEEE International conference on Embedded software, 2007

2006
Combination of Abstractions in the ASTRÉE Static Analyzer.
Proceedings of the Advances in Computer Science, 2006

2005
Abstract interpretation of programs as Markov decision processes.
Sci. Comput. Program., 2005

The ASTREÉ Analyzer.
Proceedings of the Programming Languages and Systems, 2005

Compositional Analysis of Floating-Point Linear Numerical Filters.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The Parallel Implementation of the Astrée Static Analyzer.
Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2003
Abstracting cryptographic protocols with tree automata.
Sci. Comput. Program., 2003

Abstraction of Expectation Functions Using Gaussian Distributions.
Proceedings of the Verification, 2003

A static analyzer for large safety-critical software.
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.
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).
PhD thesis, 2001

An Abstract Analysis of the Probabilistic Termination of Programs.
Proceedings of the Static Analysis, 8th International Symposium, 2001

An abstract Monte-Carlo method for the analysis of probabilistic programs.
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.
Proceedings of the Programming Languages and Systems, 2001

2000
Abstract Interpretation of Probabilistic Semantics.
Proceedings of the Static Analysis, 7th International Symposium, 2000

1999
Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief.
Proceedings of the 12th IEEE Computer Security Foundations Workshop, 1999


  Loading...