2010/07/24 by Christopher Earl, Matthew Might, Earl, Christopher +3
Computer Science · #F.3.2 #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Real-Time Systems Scheduling
paper · pdf · doi:10.48550/arxiv.1007.4268
openalex publication_date 2010/07/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Context-free approaches to static analysis gain precision over classical approaches by perfectly matching returns to call sites---a property that eliminates spurious interprocedural paths. Vardoulakis and Shivers's recent formulation of CFA2 showed that it is possible (if expensive) to apply context-free methods to higher-order languages and gain the same boost in precision achieved over first-order programs. To this young body of work on context-free analysis of higher-order programs, we contribute a pushdown control-flow analysis framework, which we derive as an abstract interpretation of a CESK machine with an unbounded stack. One instantiation of this framework marks the first polyvariant pushdown analysis of higher-order programs; another marks the first polynomial-time analysis. In the end, we arrive at a framework for control-flow analysis that can efficiently compute pushdown generalizations of classical control-flow analyses.