Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra∗

Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate methods for making the cost of inclusion certificate generation negligible. From a performance point of view, our single-representation, constraints-based implementation compares with state-of-the-art implementations. In static analysis by abstract interpretation [6], sets of reachable states, which are in general infinite or at least very large and not amenable to domain on which the analyzer applies forward (resp. backward) steps corresponding to program operations (assignments, tests...) as well as “joins ” corresponding to control points with several incoming (resp. outgoing) edges. When dealing with numerical variables in the analyzed programs, one of the simplest abstract domains consists in keeping one interval per variable, and the forward analysis is known as interval arithmetic. Interval arithmetic however does not keep track of relationships between variables. The domain of convex polyhedra [7] tracks relationships of the form i aixi. / b where the ai and b are integer (or rational) constants, the xi are rational program variables, and. / is ≤, < or =. The implementor of an abstract domain faces two hurdles: the implemen-tation should be reasonably efficient and scalable; it should be reasonably bug-free. As an example, the Parma Polyhedra Library (PPL) [1], version 1.0, which implements several relational numerical abstract domains, comprise