328 citations · 732 across the 43 of their papers we have counts for
27 papers · 1 filter
Completeness in static analysis by abstract interpretation, a personal point of view
David Monniaux
Static analysis by abstract interpretation is generally designed to be "sound", that is, it should not claim to establish properties that do not hold-in other words, not provide "f…
Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion
David Monniaux, Cyril Six
We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global su…
Fast and exact analysis for LRU caches
Claire Maïza, Valentin Touzeau, David Monniaux +1
For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that…
On the complexity of cache analysis for different replacement policies
David Monniaux, Valentin Touzeau
Modern processors use cache memory: a memory access that "hits" the cache returns early, while a "miss" takes more time. Given a memory access in a program, cache analysis consists…
Ascertaining Uncertainty for Efficient Exact Cache Analysis
Valentin Touzeau, Claire Maïza, David Monniaux +1
Static cache analysis characterizes a program's cache behavior by determining in a sound but approximate manner which memory accesses result in cache hits and which result in cache…
On the decidability of the existence of polyhedral invariants in transition systems
David Monniaux
Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties.For numerical properties, a classical class of invariants is conve…
Combining Forward and Backward Abstract Interpretation of Horn Clauses
Alexey Bakhirkin, David Monniaux
Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of s…
Model Checking of Cache for WCET Analysis Refinement
Valentin Touzeau, Claire Maïza, David Monniaux
On real-time systems running under timing constraints, scheduling can be performed when one is aware of the worst case execution time (WCET) of tasks. Usually, the WCET of a task i…
An encoding of array verification problems into array-free Horn clauses
David Monniaux, Laure Gonnord
Automatically verifying safety properties of programs is hard, and it is even harder if the program acts upon arrays or other forms of maps. Many approaches exist for verifying pro…
A simple abstraction of arrays and maps by program translation
David Monniaux, Francesco Alberti
We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar opera…
How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics
Julien Henry, Mihail Asavoae, David Monniaux +1
In systems with hard real-time constraints, it is necessary to compute upper bounds on the worst-case execution time (WCET) of programs; the closer the bound to the real WCET, the…
Implementing hash-consed structures in Coq
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases includ…
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
Alexis Fouilhé, David Monniaux, Michaël Périn
Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole st…
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
Thomas Martin Gawlitza, David Monniaux
We consider the problem of computing numerical invariants of programs, for instance bounds on the values of numerical program variables. More specifically, we study the problem of…
PAGAI: a path sensitive static analyzer
Julien Henry, David Monniaux, Matthieu Moy
We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical va…
Succinct Representations for Abstract Interpretation
Julien Henry, David Monniaux, Matthieu Moy
Abstract interpretation techniques can be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. SMT-solving techniques and spar…
Stratified Static Analysis Based on Variable Dependencies
David Monniaux, Julien Le Guen
In static analysis by abstract interpretation, one often uses widening operators in order to enforce convergence within finite time to an inductive invariant. Certain widening oper…
Modular Abstractions of Reactive Nodes using Disjunctive Invariants
David Monniaux, Martin Bodin
We wish to abstract nodes in a reactive programming language, such as Lustre, into nodes with a simpler control structure, with a bound on the number of control states. In order to…
Using Bounded Model Checking to Focus Fixpoint Iterations
David Monniaux, Laure Gonnord
Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as…
Improving Strategies via SMT Solving
Thomas Martin Gawlitza, David Monniaux
We consider the problem of computing numerical invariants of programs by abstract interpretation. Our method eschews two traditional sources of imprecision: (i) the use of widening…
Automatic modular abstractions for template numerical constraints
David Monniaux
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operatin…
Automatic Modular Abstractions for Linear Constraints
David Monniaux
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operatin…
Applying the Z-transform for the static analysis of floating-point numerical filters
David Monniaux
Digital linear filters are used in a variety of applications (sound treatment, control/command, etc.), implemented in software, in hardware, or a combination thereof. For safety-cr…
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
David Monniaux
We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism…