[PRL] Torture chamber WVH366 Wed. 19 14:30-15:30

[J. Ian Johnson]

Please come help torture me for my forthcoming talk at HOPA, an affiliated workshop with the LICS conference.

This is a 30 minute slot, so 25 minute talk with 5 minutes for questions.

Title: Concrete Semantics for Pushdown Analysis: The Essence of Summarization
Speaker: J. Ian Johnson
Abstract:
Pushdown analysis is better than finite-state analysis in precision 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.