CTL
15 October 2015 - 14h00
Revisiting the abstract domain of polyhedra: constraints-only representation and formal proof (Phd Defense)
by Alexis Fouilhe from Verimag
Abstract: The work reported in this thesis revisits in two ways the abstract domain of
polyhedra used for static analysis of programs. First, strong guarantees are
provided on the soundness of the operations on polyhedra, by using of the Coq
proof assistant to check the soundness proofs. The means used to ensure cor-
rectness don’t hinder the performance of the resulting Verimag Polyhedra
Library (VPL). It is built on the principle of result verification: computations
are performed by an untrusted oracle and their results are verified by a checker
whose correctness is proved in Coq. In order to make verification cheap, the
oracle computes soundness witnesses along with the results. The other distin-
guishing feature of VPL is that it relies only on the constraint representation
of polyhedra, as opposed to the common practice of using both constraints and
generators. Despite this unusual choice, VPL turns out to be a competitive
abstract domain of polyhedra, performance-wise.
As expected, the join operator of VPL, which performs the convex hull
of two polyhedra, is the costliest operator. Since it builds on the projection
operator, this thesis also investigates a new approach to performing projections,
based on parametric linear programming. A new understanding of projection
encoded as a parametric linear problem is presented. The thesis closes on a
progress report in the design of a new solving algorithm, tailored to the specifics
of the encoding so as to achieve good performance.
