# Incrementally Closing Octagons

Chawdhary, Aziem and Robbins, Ed and King, Andy (2018) Incrementally Closing Octagons. Formal Methods in System Design, . ISSN 0925-9856. E-ISSN 1572-8102. (doi:https://doi.org/10.1007/s10703-017-0314-7) (Full text available)

PDF - Publisher pdf

 Preview
PDF - Pre-print
 Preview
Official URL
https://doi.org/10.1007/s10703-017-0314-7

## Abstract

The octagon abstract domain is a widely used numeric abstract domain expressing relational information between variables whilst being both computationally efficient and simple to implement. Each element of the domain is a system of constraints where each constraint takes the restricted form $\pm x_i \pm x_j \leq c$. A key family of operations for the octagon domain are closure algorithms, which check satisfiability and provide a normal form for octagonal constraint systems. We present new quadratic incremental algorithms for closure, strong closure and integer closure and proofs of their correctness. We highlight the benefits and measure the performance of these new algorithms.

Item Type: Article Abstract interpretation, Octagons, Incremental closure Faculties > Sciences > School of Computing > Programming Languages and Systems Group Andy King 31 Oct 2017 12:42 UTC 25 May 2018 09:12 UTC https://kar.kent.ac.uk/id/eprint/64181 (The current URI for this page, for reference purposes)