Pushdown analysis is better than finite-state analysis in pre- cision and
performance. Why then have we not seen total widespread adoption of these
techniques? For one, the known techniques are technically burdened and
difficult to understand or extend. Control structure of the programming
language gets pulled into the model of computation, which makes extensions to
non-pushdown control structures, such as call/cc or shift and reset,
non-trivial. We show a derivational approach to abstract interpretation that
yields transparently sound static analyses that can precisely match calls and
returns when applied to well-known abstract machines. We show that adding
memoization and segmenting the continuation into bounded pieces leads to
machines that abstract to static analyses for context-free reachability by
simply bounding the stores. This technique allows us to derive existing, more
technically involved analyses, and a novel pushdown analysis for delimited,
composable control.
Description
[1305.3163] Concrete Semantics for Pushdown Analysis: The Essence of Summarization
%0 Generic
%1 johnson2013concrete
%A Johnson, J. Ian
%A Van Horn, David
%D 2013
%K demo
%T Concrete Semantics for Pushdown Analysis: The Essence of Summarization
%U http://arxiv.org/abs/1305.3163
%X Pushdown analysis is better than finite-state analysis in pre- cision and
performance. Why then have we not seen total widespread adoption of these
techniques? For one, the known techniques are technically burdened and
difficult to understand or extend. Control structure of the programming
language gets pulled into the model of computation, which makes extensions to
non-pushdown control structures, such as call/cc or shift and reset,
non-trivial. We show a derivational approach to abstract interpretation that
yields transparently sound static analyses that can precisely match calls and
returns when applied to well-known abstract machines. We show that adding
memoization and segmenting the continuation into bounded pieces leads to
machines that abstract to static analyses for context-free reachability by
simply bounding the stores. This technique allows us to derive existing, more
technically involved analyses, and a novel pushdown analysis for delimited,
composable control.
@misc{johnson2013concrete,
abstract = {Pushdown analysis is better than finite-state analysis in pre- cision and
performance. Why then have we not seen total widespread adoption of these
techniques? For one, the known techniques are technically burdened and
difficult to understand or extend. Control structure of the programming
language gets pulled into the model of computation, which makes extensions to
non-pushdown control structures, such as call/cc or shift and reset,
non-trivial. We show a derivational approach to abstract interpretation that
yields transparently sound static analyses that can precisely match calls and
returns when applied to well-known abstract machines. We show that adding
memoization and segmenting the continuation into bounded pieces leads to
machines that abstract to static analyses for context-free reachability by
simply bounding the stores. This technique allows us to derive existing, more
technically involved analyses, and a novel pushdown analysis for delimited,
composable control.},
added-at = {2013-05-16T17:57:14.000+0200},
author = {Johnson, J. Ian and Van Horn, David},
biburl = {https://www.bibsonomy.org/bibtex/2172aecbe34a18a87771f6f1d4d6288fe/fpeng1985},
description = {[1305.3163] Concrete Semantics for Pushdown Analysis: The Essence of Summarization},
interhash = {2f02bbafef8ba502568e4b69c6b8dc4e},
intrahash = {172aecbe34a18a87771f6f1d4d6288fe},
keywords = {demo},
note = {cite arxiv:1305.3163},
timestamp = {2013-05-16T17:57:14.000+0200},
title = {Concrete Semantics for Pushdown Analysis: The Essence of Summarization},
url = {http://arxiv.org/abs/1305.3163},
year = 2013
}