A Logical Product Approach to Zonotope Intersection

We define and study a new abstract domain which is a fine-grained combination of zonotopes with (sub-)polyhedric domains such as the interval, ocinear template or polyhedron domains. While abstract transfer functions are still rather inexpensive and accurate even for interpreting non-linear computations, we are able to also interpret tests (i.e. intersections) efficiently. This fixes a known drawback of zonotopic methods, as used for reachability analysis for hybrid systems as well as for invariant generation in abstract interpretation: intersection of zonotopes are not always zonotopes, and there is not even a best zonotopic over-approximation of the intersection. We describe some examples and an implementation of our method in the APRON library, and discuss some further interesting combinations of zonotopes with non-linear or non-convex domains such as quadratic templates and maxplus polyhedra.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Khalil Ghorbal, Eric Goubault, Sylvie Putot
• Keywords: Abstract Transfer Functions, CAV 2010, Fine-grained Combination, Hardware, Non-linear Computations