The Octagon Abstract Domain
<|reference_start|>The Octagon Abstract Domain: This article presents a new numerical abstract domain for static analysis by abstract interpretation. It extends a former numerical abstract domain based on Difference-Bound Matrices and allows us to represent invariants of the form (+/-x+/-y<=c), where x and y are program variables and c is a real constant. We focus on giving an efficient representation based on Difference-Bound Matrices - O(n2) memory cost, where n is the number of variables - and graph-based algorithms for all common abstract operators - O(n3) time cost. This includes a normal form algorithm to test equivalence of representation and a widening operator to compute least fixpoint approximations.<|reference_end|>
@article{miné2007the,
    title={The Octagon Abstract Domain},
    author={Antoine Min'e (LIENS)},
    journal={Analysis, Slicing and Transformation (AST) (10/2001) 310-319},
    year={2007},
    archivePrefix={arXiv},
    eprint={cs/0703084},
    primaryClass={cs.PL}
}