Room 206 (2nd floor, badged access)
11 décembre 2018 - 14h00
Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants
par Bibek Kabi de LIX
Abstract: We propose to extend an existing framework combining ab-
stract interpretation and continuous constraint programming for numer-
ical invariant synthesis, by using more expressive underlying abstract
domains, such as zonotopes. The original method, which relies on itera-
tive refinement, splitting and tightening a collection of abstract elements
until reaching an inductive set, was initially presented in combination
with simple underlying abstract elements, boxes and octagons. The nov-
elty of our work is to use zonotopes, a sub-polyhedric domain that shows
a good compromise between cost and precision. Zonotopes not being
closed under intersection, we had to extend the existing framework, in
addition to designing new operations on zonotopes, such as a novel split-
ting algorithm based on paving zonotopes by sub-zonotopes and paral-
lelotopes. We implemented this method on top of the APRON library,
and tested it on programs with non-linear loops that present complex,
possibly non-convex, invariants. We present some results demonstrating
both the interest of this splitting-based algorithm to synthesize invari-
ants on such programs, and the good compromise presented by its use
in combination with zonotopes with respect to its use with both simpler
domains such as boxes and octagons, and more expressive domains such
as polyhedra.
