The Octahedron Abstract Domain

hedron Abstract Domain Robert Claris´o and Jordi Cortadella Universitat Polit`ecnica de Catalunya Barcelona, Spain Abstract. An interesting area in static analysis is the study of numeric propermplex 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 nustract domain called octahedron that represents constraints of the form (±xj ± . . . ± xk ≥ c), where xi are numerical variables such that xi ≥ 0. The implementation of octahedra is based on a new kind of decision diagrams called Octahedron Decision Diagrams (OhDD).

• Type: Conference
• Year: 2004
• Where: SAS
• Authors: Robert Clarisó, Jordi Cortadella
• Keywords: Abstract Domain, Adequate Abstract Domain, Formal Methods, Hedron Abstract Domain, SAS 2004