Conference Proceedings

Dissecting widening: Separating termination from information

G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey

Programming Languages and Systems, 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1–4, 2019, Proceedings | Springer | Published : 2019


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 v..

View full abstract


Awarded by Australian Research Council

Awarded by US NSF

Funding Acknowledgements

This work was partially supported by the Australian Research Council through Discovery Early Career Researcher Award DE160100568 and US NSF grants 1528153 and 1817204.