This is a beautiful paper that anyone interested in abstract interpretation and sound static analysis probably already knows, but the core idea is quite accessible.
An abstract machine is a formalization of the concrete semantics of a programming language, and we'd like to be able to "lift" that concrete semantics to an abstract semantics: a finite (and therefore computable) over-approximation of program semantics.
However, the concrete structures of an abstract machine (most notably continuations) are themselves potentially infinite, so you can't just build a "structural abstraction" by applying the abstraction function pointwise over concrete structures -- the resulting abstraction is infinite and thus static analysis may diverge.
That's where this paper comes in: its key insight is that, by store-allocating continuations and bounding the number of store addresses, you can finitize an abstract machine such that structural abstraction works out nicely while preserving the underlying semantics.
An abstract machine is a formalization of the concrete semantics of a programming language, and we'd like to be able to "lift" that concrete semantics to an abstract semantics: a finite (and therefore computable) over-approximation of program semantics.
However, the concrete structures of an abstract machine (most notably continuations) are themselves potentially infinite, so you can't just build a "structural abstraction" by applying the abstraction function pointwise over concrete structures -- the resulting abstraction is infinite and thus static analysis may diverge.
That's where this paper comes in: its key insight is that, by store-allocating continuations and bounding the number of store addresses, you can finitize an abstract machine such that structural abstraction works out nicely while preserving the underlying semantics.