Skip to main content
Kent Academic Repository

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)

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: 04 Mar 2024 16:23 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/64181 (The current URI for this page, for reference purposes)

University of Kent Author Information

Chawdhary, Aziem.

Creator's ORCID:
CReDIT Contributor Roles:

Robbins, Ed.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:
  • Depositors only (login required):

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