Elusive but Coverable: The Recursion-Theoretic Structure of Complete Abstract Interpretations

Jul 16, 2026

Upload by Eden

We investigate local completeness and incompleteness of abstract interpretations through a recursion-theoretic lens. Local completeness relaxes global completeness by forbidding precision loss for a specific precondition, ensuring abstract computation matches the abstraction of the corresponding concrete computation and enabling compositional verification without false positives. We link static versus dynamic program analysis to uniformly decidable operations, showing dynamic cases are only uniformly decidable for trivial abstractions. We prove that programs inducing locally complete predicate transformers on non-trivial domains form an elusive productive set, not computably enumerable, and that their complements share this status under mild assumptions.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages26

Reading Time1 h 6 min

Introduction

The problem

Local completeness logic and AIR

Main results and characterization

Decidability of static vs dynamic analysis

Elusiveness, productivity, and enumerability

Decidable coverings and effective enumeration

arXiv :2607 .09 128v 1 [ cs .LO] 10 Jul 2026 Elusive but Coverable: The Recursion-Theoretic Structure of Complete Abstract Interpretations Nicklas Carpenter and Roberto Giacobazzi University of Arizona {[npcarpenter | giacobazzi](npcarpenter | giacobazzi}@arizona.edu)[}](npcarpenter | giacobazzi}@arizona.edu)[@](npcarpenter | giacobazzi}@arizona.edu)[arizona.edu](npcarpenter | giacobazzi}@arizona.edu) 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 Π02 and the second in Σ02. Unlike the usual examples of Π02 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. Keywords: Abstract interpretation · completeness · program analysis · program verification · computability theory 1 Introduction In any theory, the study of limit cases is a powerful means of exposing its conceptual structure. They mark the boundary between possibility and impossibility, distinguish essential assumptions from accidental ones, and provide idealized reference points for understanding more practical instances. Complete abstract interpretations play this role within abstract interpretation. Abstract interpretation is a general theory for specifying approximate semantics of programming languages [8], including program analysis, program logics, and program transformations as special cases. This is achieved by designing an approximate (abstract) interpreter from the semantics of a given computational system (e.g., a programming language) and an abstraction of its state space. The 2 Nicklas Carpenter and Roberto Giacobazzi abstraction, specified by the so called abstract domain, later denoted A, plays a key role in the abstract interpretation construction. It specifies precisely what information has to be retained and what can be abstracted away, with the specific goal that interpreting in the simplified abstract domain yet keeps as much information as possible to achieve our goals, e.g., proving program correctness. By construction, abstract interpretation is sound [8], meaning that if the approximate abstract interpretation of a program is correct with respect to a specification then also its concrete semantics satisfies the specification. The converse is rare and corresponds to the limit, and ideal, situation where no loss of precision is cumulated in the abstract interpretation with respect to what can be obtained by abstracting the concrete computation. When this happens we have completeness [9, 18] . Completeness clarifies which aspects of a computation can be abstracted away while preserving the ability to reason precisely about its properties. In program verification, program analysis and program logics completeness guarantees the absence of false positives, therefore making it possible to have a perfect matching between concrete and approxim

FAQs

What does local completeness guarantee in abstract interpretation?

Local completeness ensures that, for a chosen precondition, the abstract computation produces exactly the same result as abstracting the corresponding concrete computation, preventing precision loss for that case.

How does the work distinguish static from dynamic program analysis?

It characterizes the difference using uniformly decidable operations, showing that uniformly decidable behavior for dynamic analysis occurs only for trivial abstractions.

What is the recursion-theoretic status of programs inducing locally complete behavior on non-trivial domains?

The set of such programs is elusive and productive: it is not computably enumerable, and—under mild hypotheses—the complement is not computably enumerable either.

Jul 16, 2026

Upload by Eden