Sound up-to techniques and Complete abstract domains
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic

TL;DR
This paper explores the relationship between sound up-to techniques and complete abstract domains within abstract interpretation, highlighting their theoretical connection and implications for program analysis.
Contribution
It demonstrates, under reasonable assumptions, a clear link between sound up-to techniques and complete abstract domains, bridging two important concepts in static analysis.
Findings
Connection established between sound up-to techniques and complete abstract domains
Under certain assumptions, the relationship simplifies the understanding of abstract interpretation
Provides theoretical insights into the design of sound and complete analysis methods
Abstract
Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points. While abstract interpretation is always sound by definition, the soundness of up-to techniques needs some ingenuity to be proven. For completeness, the setting is switched: up-to techniques are always complete, while abstract domains are not. In this work we show that, under reasonable assumptions, there is an evident connection between sound up-to techniques and complete abstract domains.
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.
