28 citations · 42 across the 4 of their papers we have counts for
4 papers
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…
A Quantifier Elimination Algorithm for Linear Real Arithmetic
David Monniaux
We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which…
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…
The parallel implementation of the Astrée static analyzer
David Monniaux
The Astrée static analyzer is a specialized tool that can prove the absence of runtime errors, including arithmetic overflows, in large critical programs. Keeping analysis times re…