@article {19583,
	title = {Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis},
	journal = {arXiv:1105.1743 [cs]},
	year = {2011},
	note = {Comment: Communications of the ACM, Research Highlight},
	month = {2011/05/09/},
	abstract = {Predictive models are fundamental to engineering reliable software systems. However, designing conservative, computable approximations for the behavior of programs (static analyses) remains a difficult and error-prone process for modern high-level programming languages. What analysis designers need is a principled method for navigating the gap between semantics and analytic models: analysis designers need a method that tames the interaction of complex languages features such as higher-order functions, recursion, exceptions, continuations, objects and dynamic allocation. We contribute a systematic approach to program analysis that yields novel and transparently sound static analyses. Our approach relies on existing derivational techniques to transform high-level language semantics into low-level deterministic state-transition systems (with potentially infinite state spaces). We then perform a series of simple machine refactorings to obtain a sound, computable approximation, which takes the form of a non-deterministic state-transition systems with finite state spaces. The approach scales up uniformly to enable program analysis of realistic language features, including higher-order functions, tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.},
	keywords = {Computer Science - Programming Languages, F.3.2, F.4.1},
	url = {http://arxiv.org/abs/1105.1743},
	author = {David Van Horn and Might, Matthew}
}
@article {19582,
	title = {Abstracting Abstract Machines},
	journal = {arXiv:1007.4446 [cs]},
	year = {2010},
	note = {Comment: The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP{\textquoteright}10), Baltimore, Maryland, September, 2010},
	month = {2010/07/26/},
	abstract = {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{\textquoteright}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.},
	keywords = {Computer Science - Programming Languages, F.3.2, F.4.1},
	url = {http://arxiv.org/abs/1007.4446},
	author = {David Van Horn and Might, Matthew}
}
@article {19591,
	title = {Pushdown Control-Flow Analysis of Higher-Order Programs},
	journal = {arXiv:1007.4268 [cs]},
	year = {2010},
	note = {Comment: The 2010 Workshop on Scheme and Functional Programming},
	month = {2010/07/24/},
	abstract = {Context-free approaches to static analysis gain precision over classical approaches by perfectly matching returns to call sites---a property that eliminates spurious interprocedural paths. Vardoulakis and Shivers{\textquoteright}s recent formulation of CFA2 showed that it is possible (if expensive) to apply context-free methods to higher-order languages and gain the same boost in precision achieved over first-order programs. To this young body of work on context-free analysis of higher-order programs, we contribute a pushdown control-flow analysis framework, which we derive as an abstract interpretation of a CESK machine with an unbounded stack. One instantiation of this framework marks the first polyvariant pushdown analysis of higher-order programs; another marks the first polynomial-time analysis. In the end, we arrive at a framework for control-flow analysis that can efficiently compute pushdown generalizations of classical control-flow analyses.},
	keywords = {Computer Science - Programming Languages, F.3.2, F.4.1},
	url = {http://arxiv.org/abs/1007.4268},
	author = {Earl, Christopher and Might, Matthew and David Van Horn}
}
