Static Analysis of Abstract Machines
Abstracting Abstract Machines
Abstract interpretation is a fundamental concept in machine theory.We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines.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.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.
