IMAG 206
14 June 2016 - 13h30
Using abstract interpretation on Horn clauses: arrays and lists
by Julien Braine from École normale supérieure de Lyon
14 June 2016 - 13h30
Using abstract interpretation on Horn clauses: arrays and lists
by Julien Braine from École normale supérieure de Lyon
Abstract: Automatically verifying safety properties of programs is a tough problem that has been tackled
using many different approaches: rewriting systems, abstract interpretation, SMT solving.
Most techniques restrict themselves to programs operating on Boolean and integer values and
transposing them to infinite data structures such as arrays has not yet been satisfyingly achieved.
Recent work by Monniaux and Gonnord suggests to use abstract interpretation to transpose
programs containing arrays into Horn clauses that do not contain arrays. The major innovation of
their work is that they use non-linear Horn clauses allowing more expressiveness than program to
program transformations.
In this work, we first set the work of Monniaux and Gonnord in a more general frame that allows
us to extend their abstractions to convert Horn clauses with arrays to Horn clauses without arrays,
simplify the expressions they generate, and prove precision analysis on their work.
Finally we extend their abstractions so that we can the analyze lists and experiments show that
we succeed to analyze several classical examples, including selection sort, bubble sort, insertion sort.
