Skip to main content

Incrementally Closing Octagons

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

PDF - Publisher pdf

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (2MB) Preview
PDF - Pre-print
Download (598kB) Preview
Official URL


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
DOI/Identification number: 10.1007/s10703-017-0314-7
Uncontrolled keywords: Abstract interpretation, Octagons, Incremental closure
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Andy King
Date Deposited: 31 Oct 2017 12:42 UTC
Last Modified: 29 May 2019 19:45 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year