Searcharxiv⌕ Search

arXiv subjects

David Monniaux

Publications and source records attributed to David Monniaux.

At least 19 recordsLinked to original sources
arXiv2026

Max-Policy Iteration, Revisited

Max-policy iteration is an approach to computing precise numeric program invariants by successive attempts at resolving maximum operators and reduction to mathematical optimization. Mathematical optimization, though, may be expensive. Here, we show, for max-policy iteration on systems of equations over integers as well as over floating point numbers, that mathematical optimization can be replaced by plain value iteration -- which is still guaranteed to terminate. As an application, a precise bound analysis for integer or floating point variables is obtained, avoiding widening operators altogether. We also consider max-policy iteration over the rational numbers, where the right-hand sides are maxima of minima of affine combinations of unknowns. We propose min-policy iteration as an alternative to linear programming for solving the optimization problems posed by max-policy iteration. We prove that max-min policy iteration is guaranteed to return the least solution for bounded systems. We also show how to extend this algorithm to unbounded systems, and how to construct certificates of soundness as well as of optimality of the computed results.

cs.PL↗
arXiv2024

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

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 "false negatives" about possible bugs. A rarer requirement is that it should be "complete", meaning that it should be able to infer certain properties if they hold. This paper describes a number of practical issues and questions related to completeness that I have come across over the years.

cs.PL↗
arXiv2024

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers

Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the object code they run truly corresponds to its source code and that it satisfies certain properties. From a scientific and technological point of view, they are a challenge: not only a number of nontrivial invariants and algorithms must be proved to be correct, but also the implementation must be reasonably effective so that the tools operate within reasonable time. Many optimizations in compilers rely on static analysis, and thus a formally verified compiler entails formally verified static analyses.In this article, we explain some difficulties, possible solutions, design choices and trade-offs pertaining to verified static analysis, in particular when the solution of the analysis is expressed as some form of tree, map or set.

cs.LO↗
arXiv2024

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis

This volume contains * The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems. * The post-proceedings of the Tenth Workshop on Horn clauses for Verification and Synthesis (HCVS 2023). The meeting was held on April 23, 2023 at the Institut Henri Poincaré in Paris. HCVS aims to bring together researchers working in the two communities of constraint/ logic programming (e.g., ICLP and CP), program verification (e.g., CAV, TACAS, and VMCAI), and automated deduction (e.g., CADE, IJCAR), on the topics of Horn clause based analysis, verification, and synthesis.

cs.LO↗
arXiv2023

Memory Simulations, Security and Optimization in a Verified Compiler

Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout. In this article, we illustrate such reasoning on pointer allocations through memory extensions and injections, as well as fine points on undefined values, by explaining how we implemented and proved correct two security features (stack canaries and pointer authentication) and one optimization (tail recursion elimination) in the CompCert formally verified compiler.

cs.LO↗
arXiv2023

BAXMC: a CEGAR approach to Max#SAT

Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art.

cs.LO↗
arXiv2022

The Trusted Computing Base of the CompCert Verified Compiler

CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.

cs.LO↗
arXiv2022

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

Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point and fixed-bitwidth integer computations, using the Coq proof assistant and successfully integrated it into the CompCert formally verified compiler.

cs.LO↗
arXiv2022

NP$^{\#P}$ = $\exists$PP and other remarks about maximized counting

We consider the following decision problem DMAX#SAT, and generalizations thereof: given a quantifier-free propositional formula $F(\mathbf{x},\mathbf{y})$, where $\mathbf{x},\mathbf{y}$ are tuples of variables, and a bound $B$, determine if there is $\vec{x}$ such that $\#\{\mathbf{y} \mid F(\mathbf{x},\mathbf{y})\} \geq B$. This is the decision version of the problem of MAX#SAT: finding $\mathbf{x}$ and $B$ for maximal $B$.

cs.CC↗
arXiv2022

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

The static analysis of cache accesses consists in correctly predicting which accesses are hits or misses. While there exist good exact and approximate analyses for caches implementing the least recently used (LRU) replacement policy, such analyses were harder to find for other replacement policies. A theoretical explanation was found: for an appropriate setting of analysis over control-flow graphs, cache analysis is PSPACE-complete for all common replacement policies (FIFO, PLRU, NMRU) except for LRU, for which it is only NP-complete. In this paper, we show that if procedure calls are added to the control flow, then the gap widens: analysis remains NP-complete for LRU, but becomes EXPTIME-complete for the three other policies. For this, we improve on earlier results on the complexity of reachability problems on Boolean programs with procedure calls. In addition, for the LRU policy we derive a backtracking algorithm as well as an approach for using it as a last resort after other analyses have failed to conclude.

cs.AR↗
arXiv2021

Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion

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 subexpression elimination.This approach is lightweight: each pass comes with a simple and independent proof of correctness.Experiments show the approach significantly narrows the performance gap between the CompCert certified compiler and state-of-the-art optimizing compilers.Our static analysis employs an efficient yet verified hashed set structure, resulting in fast compilation.

cs.PL↗
arXiv2020

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

Parametric linear programming is a central operation for polyhedral computations, as well as in certain control applications.Here we propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems.This type of parallel applications is challenging, because several tasks mightbe computing the same region. In this paper, we are presenting thealgorithm itself with a parallel redundancy elimination algorithm, andconducting a thorough performance analysis.

cs.CG↗
arXiv2019

An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection

Polyhedral projection is a main operation of the polyhedron abstract domain.It can be computed via parametric linear programming (PLP), which is more efficient than the classic Fourier-Motzkin elimination method.In prior work, PLP was done in arbitrary precision rational arithmetic.In this paper, we present an approach where most of the computation is performed in floating-point arithmetic, then exact rational results are reconstructed.We also propose a workaround for a difficulty that plagued previous attempts at using PLP for computations on polyhedra: in general the linear programming problems are degenerate, resulting in redundant computations and geometric descriptions.

math.OC↗
arXiv2019

On the complexity of cache analysis for different replacement policies

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 in deciding whether this access is always a hit, always a miss, or is a hit or a miss depending on execution. Such an analysis is of high importance for bounding the worst-case execution time of safety-critical real-time programs.There exist multiple possible policies for evicting old data from the cache when new data are brought in, and different policies, though apparently similar in goals and performance, may be very different from the analysis point of view. In this paper, we explore these differences from a complexity-theoretical point of view. Specifically, we show that, among the common replacement policies, LRU (Least Recently Used) is the only one whose analysis is NP-complete, whereas the analysis problems for the other policies are PSPACE-complete.

cs.PL↗
arXiv2018

Fast and exact analysis for LRU caches

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 result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable. The state-of-the-art in LRU cache analysis presents a tradeoff between precision and analysis efficiency: The classical approach to analyzing programs running on LRU caches, an abstract interpretation based on a range abstraction, is very fast but can be imprecise. An exact analysis was recently presented, but, as a last resort, it calls a model checker, which is expensive. In this paper, we develop an analysis based on abstract interpretation that comes close to the efficiency of the classical approach, while achieving exact classification of all memory accesses as the model-checking approach. Compared with the model-checking approach we observe speedups of several orders of magnitude. As a secondary contribution we show that LRU cache analysis problems are in general NP-complete.

cs.PL↗
arXiv2018

Ascertaining Uncertainty for Efficient Exact Cache Analysis

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 misses. Such information is valuable in optimizing compilers, worst-case execution time analysis, and side-channel attack quantification and mitigation.Cache analysis is usually performed as a combination of `must' and `may' abstract interpretations, classifying instructions as either `always hit', `always miss', or `unknown'. Instructions classified as `unknown' might result in a hit or a miss depending on program inputs or the initial cache state. It is equally possible that they do in fact always hit or always miss, but the cache analysis is too coarse to see it.Our approach to eliminate this uncertainty consists in (i) a novel abstract interpretation able to ascertain that a particular instruction may definitely cause a hit and a miss on different paths, and (ii) an exact analysis, removing all remaining uncertainty, based on model checking, using abstract-interpretation results to prune down the model for scalability.We evaluated our approach on a variety of examples; it notably improves precision upon classical abstract interpretation at reasonable cost.

cs.PL↗
arXiv2018

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

Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties.For numerical properties, a classical class of invariants is convex polyhedra: solution sets of system of linear (in)equalities.Forty years of research on convex polyhedral invariants have focused, on the one hand, on identifying "easier" subclasses, on the other hand on heuristics for finding general convex polyhedra.These heuristics are however not guaranteed to find polyhedral inductive invariants when they exist.To our best knowledge, the existence of polyhedral inductive invariants has never been proved to be undecidable.In this article, we show that the existence of convex polyhedral invariants is undecidable, even if there is only one control state in addition to the "bad" one.The question is still open if one is not allowed any nonlinear constraint.

cs.PL↗