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)

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

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)