How Fitting is Your Abstract Domain?

Abstract interpretation offers sound and decidable approximations for undecidable queries related to program behavior. The effectiveness of an abstract domain is entirely reliant on the abstract domain itself, and the worst-case scenario is when the abstract interpreter provides a response of “don’t know", indicating that anything could 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 level of precision that is forfeited when performing computations within the abstract domain. Our focus is on the domain’s ability to express program behaviour, which we refer to as adequacy. In this paper, we present a domain refinement strategy towards adequacy and a simple sound proof system for adequacy, designed to determine whether an abstract domain is capable of providing 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.