Polyhedron over-approximation for complexity reduction in static analysis

Abstract

Polyhedra are widely used in the verification of numerical programs. Specially, in the field of static analysis by abstract interpretation to express the program invariants. Polyhedra make the analysis very expressive but also very time consuming. That cost is mostly due to the minimization function, which is used to maintain polyhedra in their minimal representation without redundant constraints or generators. In this article, we propose method to over-approximate a polyhedron by minimizing the loss of accuracy. The idea is to find a good trade off between accuracy and execution time. The proposed method is applied as an alternative to the minimization function for the template polyhedra abstract domain.