Computer Science – Programming Languages
Scientific paper
2011-07-18
Computer Science
Programming Languages
Scientific paper
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.
Horn David Van
Might Matthew
No associations
LandOfFree
Systematic Abstraction of Abstract Machines does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Systematic Abstraction of Abstract Machines, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Systematic Abstraction of Abstract Machines will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-272528