AI summaryⓘ
The authors study a concept called local completeness in abstract interpretation, which means that for certain program parts, analyzing the program abstractly gives exactly the same results as analyzing it concretely. They explore the differences between static and dynamic program analysis in terms of what can be decided mechanically and show that dynamic analysis is only uniformly decidable in trivial cases. They prove that determining which programs are locally complete for a certain abstraction is very complex from a recursion theory viewpoint, making it impossible to list all such programs directly. However, they find ways to cover these complex classes with simpler, decidable sets, enabling practical enumeration from outside the class.
abstract interpretationlocal completenessprogram analysisstatic analysisdynamic analysisrecursion theorydecidabilitycomputably enumerablepredicate transformerprogram transformation
Authors
Nicklas Carpenter, Roberto Giacobazzi
Abstract
We study local completeness and incompleteness of abstract interpretations from a recursion-theoretic perspective. Local completeness weakens global completeness and captures the absence of precision loss for a specific precondition: abstract computation yields exactly what is obtained by abstracting the corresponding concrete computation. This enables compositional reasoning and rules out false positives in verification. We characterize the distinction between static and dynamic program analysis in terms of uniformly decidable operations and observe that the latter is uniformly decidable only for trivial abstractions. We then prove that the class of programs inducing a predicate transformer that is locally complete for a given non-trivial abstract domain is elusive in a precise recursion-theoretic sense: it is a productive set, hence not computably enumerable, and, under mild hypotheses, the same holds for its complement. In particular, the first class lies in $Π^0_2$ and the second in $Σ^0_2$. Unlike the usual examples of $Π^0_2$ properties, we show that the classes of locally complete programs admit decidable coverings. This makes it possible to construct, via program transformation, an effective enumeration of a representative subset of programs that entirely covers this class -- capturing from the outside a class that eludes enumeration from within.