Abstracting Abstract Machines

Details Abstracting Abstract Machines Abstracting Abstract Machines

2010-07-26

arxiv.org/abs/1007.4446v2

Computer Science

Programming Languages

The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP'10), Baltimore, Maryland, September, 2010

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. 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 we call 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.

Affiliated with

Also associated with

No associations

Rating

Abstracting 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 Abstracting Abstract Machines, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Abstracting Abstract Machines will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-559188