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 DecDisplayed time zone: Osaka, Sapporo, Tokyo change
10:30 - 12:00 | Program Analysis and VerificationResearch Papers at online Chair(s): Benjamin Delaware Purdue University | ||
10:30 30mTalk | Declarative Stream Runtime Verification (hLola) Research Papers Martin Ceresa UNR - CIFASIS - CONICET, Felipe Gorostiaga IMDEA Software Institute, César Sánchez IMDEA Software Institute | ||
11:00 30mTalk | A Set-Based Context Model for Program Analysis Research Papers Zachary Palmer Swarthmore College, Scott F. Smith The Johns Hopkins University, Leandro Facchinetti The Johns Hopkins University, Ayaka Yorihiro Cornell University, Ke Wu Johns Hopkins University | ||
11:30 30mTalk | Formal Verification of Atomicity Requirements for Smart Contracts Research Papers Ning Han Capital Normal University, Ximeng Li Capital Normal University, Guohui Wang Capital Normal University, Beijing, China, Zhiping Shi Capital Normal University, Yong Guan Capital Normal University, Beijing, China |