  We describe a derivational approach to abstract interpretation that yields
novel and transparently sound static analyses when applied to well-established
abstract machines for higher-order and imperative programming languages. To
demonstrate the technique and support our claim, we transform the CEK machine
of Felleisen and Friedman, a lazy variant of Krivine's machine, and the
stack-inspecting CM machine of Clements and Felleisen into abstract
interpretations of themselves. The resulting analyses bound temporal ordering
of program events; predict return-flow and stack-inspection behavior; and
approximate the flow and evaluation of by-need parameters. For all of these
machines, we find that a series of well-known concrete machine refactorings,
plus a technique of store-allocated continuations, leads to machines that
abstract into static analyses simply by bounding their stores. We demonstrate
that the technique scales up uniformly to allow static analysis of realistic
language features, including tail calls, conditionals, side effects,
exceptions, first-class continuations, and even garbage collection. In order to
close the gap between formalism and implementation, we provide translations of
the mathematics as running Haskell code for the initial development of our
method.

Programming Languages