Speeding up Polyhedral Analysis by Identifying Common Constraints

Sets of linear inequalities are an expressive reasoning tool for approximating the reachable states of a program. However, the most precise way to join two states is to calculate the convex hull of the two polyhedra that are represented by the inequality sets, an operation that is exponential in the dimension of the polyhedra. We investigate how similarities in the two input polyhedra can be exploited to improve the performance of this costly operation. In particular, we discuss how common equalities and certain inequalities can be omitted from the calculation without affecting the result. We expose a maximum of common equalities and inequalities by converting the polyhedra into a normal form and give experimental evidence of the merit of our method.