Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Tue 1 Dec 2020 11:00 - 11:30 at online - Program Analysis and Verification Chair(s): Benjamin Delaware

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

Displayed 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
30m
Talk
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
30m
Talk
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
30m
Talk
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