IMAG 206
7 octobre 2016 - 14h00
Cell morphing: from array programs to array-free Horn clauses
par David Monniaux de CNRS / VERIMAG
7 octobre 2016 - 14h00
Cell morphing: from array programs to array-free Horn clauses
par David Monniaux de CNRS / VERIMAG
Abstract: Automatically verifying safety properties of programs is hard. Many approaches exist for verifying
programs operating on Boolean and integer values (e.g. abstract interpretation, counterexample-guided
abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties. Our work addresses that issue with a powerful and flexible abstraction, parametric both in precision and in the back-end analysis used.
From our programs with arrays, we generate nonlinear Horn clauses over scalar variables only,
in a common format with clear and unambiguous logical semantics, for which there exist several
solvers. We thus avoid the use of solvers operating over arrays, which are still very immature.
Experiments with our prototype vaphor show that this approach can prove automatically and
without user annotations the functional correctness of several classical examples, including selection sort, bubble sort, insertion sort, as well as examples from literature on array analysis.
