Synthesizing invariants : a constraint programming approach based on zonotopic abstraction

Overview & Synopsis

Dynamical systems are mathematical models for describing temporal evolution of the state of a system. There are two classes of dynamical systems relevant to this thesis: discrete and continuous. In discrete dynamical systems (or classical computer programs), the state evolves in discrete time steps, as described by difference equations. In continuous dynamical systems, the state of the system is a function of continuous time, characterized by differential equations. When we analyze the behavior of a dynamical system, we usually want to make sure that it satisfies a safety property expressing that nothing bad happens. An example of a safety property of programs is the absence of arithmetic overflows. In this thesis, we design a framework related to the automatic verification of the safety properties of programs. Proving that a program satisfies a safety property of interest involves an invariance argument. We develop an algorithm for inferring invariants more precisely inductive invariants (properties which hold during the initial state, remains stable under the program evolution, and hence hold always due to induction) for numerical programs. A traditional approach for finding inductive invariants in programs is abstract interpretation (AI) that interprets the states of a program in an abstract domain (intervals, polyhedra, octagon, zonotopes) of choice. This choice is made based on the property of interest to be inferred. Using the AI framework, inductive invariant can be computed as limits of iterations of functions. However, for abstract domains which feature infinite increasing chain, for instance, interval, these computations may fail to converge. Then, the classical solution would be to withdraw that particular domain and in its place redesign a new abstract domain which can represent the shape of the invariant. One may also use convergence techniques like widening to enforce convergence, but this may come at the cost of precision. Another approach called constraint programming (CP), can be used to find invariants by translating a program into constraints and solving them by using constraint solvers. Constraints in CP primarily operate on domains that are either discrete or continuous. Classical continuous constraint programming corresponds to interval domain and can approximate a complex shape invariant by a set of boxes, for instance, upto a precision criterion. An existing framework combines AI and continuous CP inspired by iterative refinement, splitting and tightening a collection of abstract elements. This was initially presented in combination with simple underlying abstract elements, boxes and octagons. The novelty of our work is to extend this framework by using zonotopes, a sub-polyhedric domain that shows a good compromise between cost and precision. However, zonotopes are not closed under intersection, and we had to extend the existing framework, in addition to designing new operations on zonotopes. We introduce a novel splitting algorithm based on tiling zonotopes by sub-zonotopes and parallelotopes. We also propose few alternative operators to the existing ones for a better efficiency of the method. We implemented these operations 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 the interest of this splitting-based algorithm to synthesize invariants on such programs. This algoritm also shows a good compromise 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 like polyhedra. Finally, we discuss the extension of the approach to infer positive and negative invariant sets for dynamical systems.