POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

We study “the best of abstract interpretations”, namely, the best possible abstract interpretations of programs. Abstract interpretations of programs on a given abstract domain A are inductively defined by composing abstract transfer functions for the basic commands, such as assignments and Boolean guards. However, abstract interpretation is not compositional: even if the abstract transfer functions of the basic commands are the best possible in A this does not imply that the whole inductive abstract interpretation of a program P is still the best in A. When this happens we are in the optimal scenario where the abstract interpretation of P coincides with the abstraction of the concrete interpretation of P. Our main contributions are threefold. Firstly, we investigate the computability properties of the class of programs having the best possible abstract interpretation on a fixed abstract domain A. We show that this class is, in general, not straightforward and not recursive. We also prove the impossibility of achieving the best possible abstract interpretation of any program by an effective compilation. Secondly, we show that given an abstract interpretation of a program P on an abstract domain A, this domain cannot be minimally refined or simplified to attain the best possible abstract interpretation of P. These results show that the program property of having the best possible abstract interpretation is not trivial and, in general, hard to achieve. We then show how to prove that the abstract interpretation of a program is indeed the best possible one. This is achieved using a program logic parameterized on A which infers triples [pre]_A P [post]_A. These triples encode that the inductive abstract interpretation of P on A with abstract input pre ∈ A gives post ∈ A as abstract output and this is the best possible in A.