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
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