Both the precision and performance of abstract interpreters can greatly be improved through the integration of abstract garbage collection (GC). Unfortunately, for abstract interpreters that do not explicitly model the stack (e.g., abstract definitional interpreters), this integration has proven cumbersome. Existing approaches either fail to exploit the full precision and performance benefits of abstract GC and pushdown control flow, and/or require complicated modifications to the abstract interpreter. In addition, the lack of global store widening, which is incompatible with abstract GC, often remains an obstacle for scalability.

In this work, we present delta store semantics (DSS), offering a novel yet simple approach to integrate abstract GC into big-step abstract definitional interpreters. DSS makes a simple change to the standard big-step language semantics, returning a delta store (representing changes to the original store) instead of an updated store, enabling the integration of a single evaluation rule to interleave GC into its semantics. Importantly, we show that DSS not only preserves the advantages of big-step abstract interpreters and abstract GC, but in fact can exploit greater precision benefits (due to more aggressive GC). We formulate this claim as a theorem, for which we provide both a mechanised proof in Rocq, as well as empirical evidence. Finally, we propose a new form of store widening for DSS, which tackles the scalability issues of abstract interpreters employing abstract GC without store widening. The result is similar to the traditional notion of flow sensitivity in data-flow analyses.