Skip to main content

Incrementally Closing Octagons

Chawdhary, Aziem, Robbins, Ed, King, Andy (2019) Incrementally Closing Octagons. Formal Methods in System Design, 54 (2). pp. 232-277. ISSN 0925-9856. E-ISSN 1572-8102. (doi:10.1007/s10703-017-0314-7) (KAR id:64181)

PDF Publisher pdf
Language: English


Click to download this file (2MB) Preview
[thumbnail of 10.1007%2Fs10703-017-0314-7.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF Pre-print
Language: English
Click to download this file (598kB) Preview
[thumbnail of main.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
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 ±xi±xj≤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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 31 Oct 2017 12:42 UTC
Last Modified: 16 Feb 2021 13:49 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/64181 (The current URI for this page, for reference purposes)
King, Andy: https://orcid.org/0000-0001-5806-4822
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.