Abstracting abstract machines

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