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 - 12:00: Program Analysis and VerificationResearch Papers at online Chair(s): Benjamin DelawarePurdue University | |||
10:30 - 11:00 Talk | Declarative Stream Runtime Verification (hLola) Research Papers Martin CeresaUNR - CIFASIS - CONICET, Felipe GorostiagaIMDEA Software Institute, César SánchezIMDEA Software Institute | ||
11:00 - 11:30 Talk | A Set-Based Context Model for Program Analysis Research Papers Zachary PalmerSwarthmore College, Scott F. SmithThe Johns Hopkins University, Leandro FacchinettiThe Johns Hopkins University, Ayaka YorihiroCornell University, Ke WuJohns Hopkins University | ||
11:30 - 12:00 Talk | Formal Verification of Atomicity Requirements for Smart Contracts Research Papers Ning HanCapital Normal University, Ximeng LiCapital Normal University, Guohui WangCapital Normal University, Beijing, China, Zhiping ShiCapital Normal University, Yong GuanCapital Normal University, Beijing, China |