Write a Blog >>
Sat 25 Jan 2020 16:07 - 16:40 at Orleans - Analysis, verification, blame Chair(s): Niki Vazou

The designers of static analyses used in industry often try to reduce the number of false positives reported by the analysis through increased engineering effort, user-provided annotations, and/or weaker soundness guarantees. To produce a static analysis with little engineering effort, reduced false positives, and strong soundness guarantees in a principled way, we adapt the Abstracting Gradual Typing'' framework to the abstract-interpretation based program analysis setting. As a case study, we take a simple static dataflow analysis that relies on user-provided annotations and has nullability lattice $N \sqsubset \top$ (where $N$ meansdefinitely not null'' and $\top$ means possibly null'') and extend it by adding $?$ as a third abstract value. The question mark explicitly representsoptimistic uncertainty'' in the analysis itself, supporting a formal soundness property and the ``gradual guarantees'' laid out in the gradual typing literature. To evaluate our gradual null-pointer analysis, we implement it as a Facebook Infer checker and compare it against the existing null checkers in Facebook Infer. A preliminary set of experiments show evidence of reduced false positives. We then generalize this example into a system that gradualizes any dataflow analysis in the same way: augmenting the lattice while retaining the properties that permit it to be used in the standard dataflow analysis fixpoint algorithm.

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 17:45
Analysis, verification, blameWGT at Orleans
Chair(s): Niki Vazou IMDEA Software Institute
15:35
32m
Talk
Gradual Verification of Recursive Heap Data Structures
WGT
Jenna Wise Carnegie Mellon University, Johannes Bader Facebook, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
Pre-print
16:07
33m
Talk
Gradual Program Analysis
WGT
Samuel Estep Liberty University, Jenna Wise Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Facebook, Joshua Sunshine Carnegie Mellon University
Pre-print
16:40
10m
Break
Minibreak
WGT

16:50
30m
Talk
Blame tracking at higher fidelity
WGT
Jakub Zalewski University of Edinburgh, James McKinna University of Edinburgh, J. Garrett Morris University of Kansas, USA, Philip Wadler University of Edinburgh, UK
Pre-print
17:20
25m
Day closing
Discussion on gradual typing and WGT21
WGT