City Research Online

Abstract

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

Export

Downloads