Sound up-to techniques and Complete abstract domains

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.