328 citations · 732 across the 43 of their papers we have counts for
13 papers · 1 filter
The existence of polyhedral invariants is undecidable for linear systems
David Monniaux
The existence of polyhedral inductive invariants suitable for proving that a given control location is unreachable is undecidable for programs using only linear arithmetic over Z o…
BAXMC: a CEGAR approach to Max#SAT
Thomas Vigouroux, Cristian Ene, David Monniaux +2
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 p…
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic
David Monniaux, Alice Pain
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…
The Trusted Computing Base of the CompCert Verified Compiler
David Monniaux, Sylvain Boulmé
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…
Formula Slicing: Inductive Invariants from Preconditions
Egor George Karpenkov, David Monniaux
We propose a "formula slicing" method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and ma…
A Survey of Satisfiability Modulo Theory
David Monniaux
Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we expl…