The 4-Octahedron Abstract Domain

In static analysis, the choice of an adequate abstract domain is an interesting issue. In this paper, we provide a new numerical abstract domain: 4-Octahedron. It is an Octahedra subclass that infers relations of the form: { \( x \sim \alpha , x-y \sim \beta , (x-y) - (z-t) \sim \lambda \)}, such that: x, y, z and t are real variables, \(\alpha , \beta \) and \( \lambda \) are real constants and \({\sim }\in \{\le ,\ge \}\). Its precision lies between the octagons and octahedra. We construct a suitable structure for its representation, we provide normalization algorithms for computing its canonical form and we give methods to compute its transfer functions (Union, Intersection, Assignment, Projection, ...). Complexity of the implementation algorithms is proved to be polynomial.