Introspective pushdown analysis of higher-order programs

In the static analysis of functional programs, pushdown flow analabstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. This work illuminates and conquers the theoretical challenges that stand in the way of combining the power of these techniques. The challenge in marrying these techniques is not subtle: computing the reachable control states of a pushdown system relies on limiting access dursition to the top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to compute a root set, just as concrete collection does. Introspective pushdown systems resolve this conflict. Introspective pushdown systems prough access to the stack to allow abstract garbage collection, but they remain restricted enough to compute control-state reachability, thereby enabling the sound and precise product of pushdown analysis and abstract...

• Type: Journal
• Year: 2012
• Where: ICFP
• Authors: Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
• Keywords: ICFP 2012, Operational Semantics, Programming Languages, Programming Languages Processors, Theoretical Challenges