Seminar Room, ground floor (Building IMAG)
7 décembre 2017 - 14h00
Synthesizing Invariants by Solving Solvable Loops
par De Oliviera Steven de CEA-List/Verimag
Abstract: The complexity of program verification is directly dependent of the ability of analyzers to soundly handle loops. One way to overapproximate loops is to provide them inductive invariants, summing up their behavior and often providing enough information to provers. Unfortunately, even in very simple loops like linear loops (i.e. loops composed of linear assignments only) there exist no invariant up to our knowledge that allows to conclude any interesting property over the loop
(take the Syracuse sequence for example). In the mean time there exist more complex loops, like polynomial loops, on which we can not only infer every inductive polynomial invariant it admits, but also get invariants that are strictly equivalent to the loop (for example, the sum of the squares admits an exact invariant that sums up the whole loop). The questions are: what can we infer from linear loops, and is there a subclass of polynomial problems over which we similarly deduce information from ?
In this talk, I will present a new technique to infer invariant on a specific class of polynomial loops called solvable loops. This class of loops has the particular property of being linearizable, i.e. there exist a linear transformation computing the same image. I will show that this class of loops is exactly the set of linearizable loops. From the newly generated linear loops, I present a new method based on basic and low complexity linear algebra algorithms that infer every linear invariant of a linear loop. Thanks to the linearization procedure, it also generates polynomial invariants. Then, I will present different extensions of this technique : how to handle conditions, nested loops, and non deterministic assignments. Finally, I will present Pilat, the open-source Frama-C plugin implementing the technique and all its extensions for the verification of C programs, followed by a demonstration on multiple examples from the literature.
