Dissecting widening: separating termination from information

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

Abstract

Widening ensures or accelerates convergence of a program analysis, and sometimes contributes a guarantee of soundness that would otherwise be absent. In this paper we propose a generalised view of widening, in which widening operates on values that are not necessarily elements of the given abstract domain, although they must be in a correspondence, the details of which we spell out. We show that the new view generalizes the traditional view, and that at least three distinct advantages flow from the generalization. First, it gives a handle on “compositional safety”, the problem of creating widening operators for product domains. Second, it adds a degree of flexibility, allowing us to define variants of widening, such as delayed widening, without resorting to intrusive surgery on an underlying fixpoint engine. Third, it adds a degree of robustness, by making it difficult for an analysis implementor to make certain subtle (syntactic vs semantic) category mistakes. The paper supports these claims with examples. Our proposal has been implemented in a state-of-the-art abstract interpreter, and we briefly report on the changes that the revised view necessitated.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication17th Asian Symposium, APLAS 2019 Nusa Dua, Bali, Indonesia, December 1–4, 2019 Proceedings
EditorsAnthony Widjaja Lin
Place of PublicationCham Switzerland
PublisherSpringer
Pages95-114
Number of pages20
ISBN (Electronic)9783030341756
ISBN (Print)9783030341749
DOIs
Publication statusPublished - 2019
EventAsian Symposium on Programming Languages and Systems 2019 - Bali, Indonesia
Duration: 1 Dec 20194 Dec 2019
Conference number: 17th
https://conf.researchr.org/series/aplas

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11893
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceAsian Symposium on Programming Languages and Systems 2019
Abbreviated titleAPLAS 2019
CountryIndonesia
City Bali
Period1/12/194/12/19
Internet address

Cite this

Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2019). Dissecting widening: separating termination from information. In A. W. Lin (Ed.), Programming Languages and Systems : 17th Asian Symposium, APLAS 2019 Nusa Dua, Bali, Indonesia, December 1–4, 2019 Proceedings (pp. 95-114). (Lecture Notes in Computer Science; Vol. 11893 ). Springer. https://doi.org/10.1007/978-3-030-34175-6_6