Incremental Closure for Systems of Two Variables Per Inequality
- Submitting institution
-
City, University of London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 804
- Type
- D - Journal article
- DOI
-
10.1016/j.tcs.2018.12.001
- Title of journal
- Theoretical Computer Science
- Article number
- -
- First page
- 1
- Volume
- 768
- Issue
- -
- ISSN
- 0304-3975
- Open access status
- Compliant
- Month of publication
- December
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The TVPI abstract domain and its subclasses, in particular Octagons, have been widely used in formal verification of software. Octagons have been implemented using fixed sized matrices, but this makes them memory hungry. The significance of this paper is that it shows how alternative representations using less space can be derived, whilst giving rigorous underpinning to the algorithms. The theoretical work presented in this paper is supported by a publicly available code base.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
