In program analysis, the design of context models is an understudied topic. This paper presents a study of context models for higher-order program analyses and develops new approaches. We develop a context model which equates control flows with the same set of call sites on the program stack, guaranteeing termination without the arbitrary cutoffs which cause imprecision in existing models. We then apply a selective polyinstantiation technique to avoid exponential growth.
We evaluate this model and existing models across multiple higher-order program analysis families. Existing demand-driven analyses cannot support the set model, so we construct a demand-driven analysis, Plume, which can. Our experiments demonstrate that the set-based model is tractable and expressive on representative functional programs for both forward- and demand-driven functional analyses.
Tue 1 Dec Times are displayed in time zone: Osaka, Sapporo, Tokyo change
|10:30 - 11:00|
|Declarative Stream Runtime Verification (hLola)|
|11:00 - 11:30|
|A Set-Based Context Model for Program Analysis|
|11:30 - 12:00|
|Formal Verification of Atomicity Requirements for Smart Contracts|