The octagon abstract domain

By Antoine Miné. Proceedings Eighth Working Conference on Reverse Engineering, 2001

1,035 citations recorded by the source corpus.

This article presents the octagon abstract domain, a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form ± X ± Y ≤ c where X and Y range among program variables and c is a constant in ℤ, ℚ, or ℝ automatically inferred. Abstract elements are represented using modified Difference Bound Matrices and we use a normalization algorithm loosely based on the shortest-path closure to compute canonical representations and construct best-precision abstract transfer functions. We achieve a quadratic memory cost per abstract element and a cubic worst-case time cost per abstract operation, with respect to the number of program variables.In terms of cost and precision, our domain is in between the well-known fast but imprecise interval domain and the costly polyhedron domain. We show that it is precise enough to treat interesting examples requiring relational invariants, and hence, out of the reach of the interval domain. We also present a packing strategy that allows scaling our domain up to large programs by tuning the amount of relationality. The octagon domain was incorporated into the ASTRÉE industrial-strength static analyzer and was key in proving the absence of run-time errors in large critical embedded flight control software for Airbus planes.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Hardware and Architecture

View Paper: https://www.semanticscholar.org/paper/602218cb720970fc25e1a6142e27836137e97e55

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Hardware and Architecture

Citations in the corpus

The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems (2006, methodology): “9 Another feature of this class is that its implementation uses the strong closure algorithm introduced in [10], which has lower complexity than the one used in the Octagon Abstract Domain Library 10 [68,69].”
Fast polyhedra abstract domain (2017, background): “However, this maintenance is less challenging for the Octagon domain.”
The SeaHorn Verification Framework (2015, background): “Available abstract domains include: intervals [19], reduced product of intervals with congruences [25], DBMs [43], and octagons [44].”