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
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Click to download this file (2MB)
Preview
|
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
|
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: |
![]() |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):