Summary: 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 \((\pm x_{j}\pm... \pm x_{k} \geq c)\), where \(x_{i}\) are numerical variables such that \(x_{i} \geq 0\). The implementation of octahedra is based on a new kind of decision diagrams called Octahedron Decision Diagrams (OhDD).
For the entire collection see [Zbl 1056.68010].