A minimalistic look at widening operators
David Monniaux (VERIMAG - Imag)

TL;DR
This paper redefines the concept of widening in abstract interpretation using a minimalistic approach, representing it as a lazily constructed well-founded tree to improve understanding and correctness proofs.
Contribution
It introduces a new characterization of widening as a lazily constructed well-founded tree, simplifying the formalization in higher-order logic.
Findings
Widening sequences can be characterized as well-founded trees.
Many traditional axioms of widening are unnecessary for correctness.
The approach supports dependent type systems for correct termination.
Abstract
We consider the problem of formalizing the familiar notion of widening in abstract interpretation in higher-order logic. It turns out that many axioms of widening (e.g. widening sequences are ascending) are not useful for proving correctness. After keeping only useful axioms, we give an equivalent characterization of widening as a lazily constructed well-founded tree. In type systems supporting dependent products and sums, this tree can be made to reflect the condition of correct termination of the widening sequence.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
