Abstract domain adequacy

Abstract interpretation offers sound and decidable approximations for undecidable queries related to program behavior. The effectiveness of an abstract domain primarily relies on the abstract domain itself, and the worst-case scenario is when the abstract interpreter responds with “don’t know”, indicating that anything can happen during runtime. Conversely, a desirable outcome is when the abstract interpreter provides information that exceeds a specified level of precision, resulting in a more precise answer. The concept of completeness relates to the precision level forfeited when performing computations within the abstract domain. We focus on the domain’s ability to express program behavior, which we refer to as adequacy. This paper presents a domain refinement strategy toward adequacy and a simple, sound proof system for adequacy designed to determine whether an abstract domain can provide satisfactory responses to specified program queries. Notably, this proof system is both language- and domain-agnostic and can be readily incorporated to support static program analysis.