Abstracting abstract machines

DOI10.1145/1863543.1863553MaRDI QIDQ5176929zbMATH OpenOpenAlexFDO

Authors David van Horn, Matthew Might

Publication date 5 March 2015

Published in Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.4446, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.170.9795

zbMATH Keywords

abstract interpretationabstract machines

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

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'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.

Recommendations

• Systematic abstraction of abstract machines
• Distilling abstract machines
• Optimizing abstract abstract machines
• From operational semantics to abstract machines
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2090723
• Deriving a lazy abstract machine
• From outermost reduction semantics to abstract machine
• scientific article; zbMATH DE number 3952011
• The categorical abstract machine

Cited in

(23)

• scientific article; zbMATH DE number 2090723 (Why is no real title available?)
• Distilling abstract machines
• Liberate abstract garbage collection from the stack by decomposing the heap
• Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence
• The linear abstract machine
• Abstract allocation as a unified approach to polyvariance in control-flow analyses
• Logic Programming
• Run-time type computations in the Warren Abstract machine
• Systematic abstraction of abstract machines
• Automating the functional correspondence between higher-order evaluators and abstract machines
• Abstraction of hardware construction
• Result invalidation for incremental modular analyses
• An abstract machine for the old value retrieval
• Abstract interpreters for free
• Logical approximation for program analysis
• Optimizing abstract abstract machines
• The Vienna abstract machine
• Higher order symbolic execution for contract verification and refutation
• Higher-order model checking in direct style
• A generative methodology for the design of abstract machines
• Modular, higher order cardinality analysis in theory and practice
• The categorical abstract machine
• The York Abstract Machine

This page was built for publication: Abstracting abstract machines

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5176929)