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
8 papers · 1 filter
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…
Program Analysis with Local Policy Iteration
George Karpenkov, David Monniaux, Philipp Wendler
We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterati…
On Practical SMT-Based Type Error Localization
Zvonimir Pavlinovic, Tim King, Thomas Wies
Compilers for statically typed functional programming languages are notorious for generating confusing type error messages. When the compiler detects a type error, it typically rep…
On Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King +2
Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automat…
Certified Roundoff Error Bounds Using Semidefinite Programming
Victor Magron, George Constantinides, Alastair Donaldson
Roundoff errors cannot be avoided when implementing numerical programs with finite precision. The ability to reason about rounding is especially important if one wants to explore a…
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…