Synthesizing invariants: a constraint programming approach based on zonotopic abstraction

Seminar talk titled Synthesizing invariants: a constraint programming approach based on zonotopic abstraction

Title Of the Talk: Synthesizing invariants: a constraint programming approach based on zonotopic abstraction
Speaker: Bibek Kabi
Host Faculty: Dr. Ramakrishna Upadrasta
Date &Time: Friday, 6th August 2021 12:00 - 13:00 Hrs

Abstract:

We propose to extend an existing framework combining abstract interpretation and continuous constraint programming for numerical invariant synthesis, by using more expressive underlying abstract domains, such as zonotopes. The original method, which relies on iterative 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 novelty of our work is to use zonotopes, a sub-polyhedric domain that shows a good compromise between cost and precision. As zonotopes are not closed under intersection, we had to extend the existing framework, in addition to designing new operations on zonotopes, such as a novel splitting algorithm based on paving zonotopes by sub-zonotopes and parallelotopes. 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 invariants 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.

Speaker Profile:

Bibek Kabi currently working as a research engineer in TechViz (a virtual reality company based in Paris) received his PhD from Ecole Polytechnique, CNRS, Institut Polytechnique de Paris, prepared under the supervision of Prof. Eric Goubault and Prof. Sylvie Putot at Computer Laboratory of Ecole Polytechnique (LIX) 91128 Palaiseau, France. During his PhD he was also supervised by Prof. Antoine Miné from Université Pierre et Marie Curie, Paris. His thesis is dedicated to the study of combining abstract interpretation (mostly zonotopic) and constraint programming for synthesizing invariants. His PhD thesis can be downloaded through the link https://tel.archives-ouvertes.fr/tel-02925914/. He received his MS (by research) degree from Indian Institute of Technology Kharagpur. His research interests include program verification based on zonotope abstraction, floating-point and fixed-point arithmetic, optimization of fixed-point formats in numerical programs, numerical linear algebra, data science and machine learning.

Date:
Friday, 6th August 2021 12:00 - 13:00 Hrs