City Research Online

Widening for Systems of Two Variables Per Inequality

Howe, J. M. ORCID: 0000-0001-8013-6941 & Nyx Brain, M. (2023). Widening for Systems of Two Variables Per Inequality. In: CEUR Workshop Proceedings. 8th SC-Square Workshop, 28 Jul 2023, Tromsø, Norway.


The abstract interpretation approach to program verification involves symbolically calculating fixpoints over lattices. Integral to these fixpoint calculations is an operation called widening, which discards information in order to move up the lattice so as to ensure termination, as well as potentially aiding efficiency. Abstract interpretation often uses lattices of numeric constraints where the number of variables allowed in a constraint is restricted, called weakly relational domains. This paper is concerned with the application of widening with weakly relational domains. One particular point of interest is the problematic interaction between widening and the maintenance of a closed form for weakly relational domains. The solution to this problem uses entailment, which essentially involves satisfiability checking for numeric constraints.

Publication Type: Conference or Workshop Item (Paper)
Additional Information: Copyright © 2023 for the individual papers by the papers' authors.
Publisher Keywords: Abstract Interpretation, Weakly Relational Domains, Widening
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Science & Technology > Computer Science
[thumbnail of wideningTVPI.pdf]
Text - Published Version
Available under License Creative Commons: Attribution International Public License 4.0.

Download (1MB) | Preview


Add to AnyAdd to TwitterAdd to FacebookAdd to LinkedinAdd to PinterestAdd to Email


Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login