An interesting area in static analysis is the study of numeric properties. Complex properties can be analyzed using abstract interpretation, provided that an adequate abstract domain is defined. Each domain can represent and manipulate a family of properties, providing a different trade-off between the precision and complexity of the analysis. The contribution of this paper is a new numeric abstract domain called octahedron that represents constraints of the form (±xj± … ± xk# c), where xiare numerical variables such that xi# 0. The implementation of octahedra is based on a new kind of decision diagrams called Octahedron Decision Diagrams (OhDD).

Peer Reviewed