211 citations
- Université Grenoble AlpesFR49 papers
- Centre National de la Recherche ScientifiqueFR44 papers
- Institut polytechnique de GrenobleFR12 papers
- Université Joseph FourierFR7 papers
- FortissDE4 papers
- Institut des langues et cultures d'Europe, Amérique, Afrique, Asie et AustralieFR4 papers
- Institut national de recherche en sciences et technologies du numériqueFR4 papers
- Aalto UniversityFI3 papers
- Commissariat à l'Énergie Atomique et aux Énergies AlternativesFR3 papers
- École Polytechnique Fédérale de LausanneCH3 papers
- Laboratoire d'Informatique de GrenobleFR3 papers
- LIP6FR3 papers
6 papers · 1 filter
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…
Towards Efficient Active Learning of PDFA
Franz Mayr, Sergio Yovine, Federico Pan +2
We propose a new active learning algorithm for PDFA based on three main aspects: a congruence over states which takes into account next-symbol probability distributions, a quantiza…
NP = PP and other remarks about maximized counting
David Monniaux
We consider the following decision problem DMAX#SAT, and generalizations thereof: given a quantifier-free propositional formula , where $\mathbf{x},\mathb…
The complexity gap in the static analysis of cache accesses grows if procedure calls are added
David Monniaux
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 implement…
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…