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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 17:45: WGT - Analysis, verification, blame at Orleans
Chair(s): Niki VazouIMDEA Software Institute
wgt-2020-papers15:35 - 16:07
Jenna WiseCarnegie Mellon University, Johannes BaderFacebook, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University
wgt-2020-papers16:07 - 16:40
Samuel EstepLiberty University, Jenna WiseCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Johannes BaderFacebook, Joshua SunshineCarnegie Mellon University
wgt-2020-papers16:40 - 16:50
wgt-2020-papers16:50 - 17:20
Jakub ZalewskiUniversity of Edinburgh, James McKinnaUniversity of Edinburgh, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK
wgt-2020-papers17:20 - 17:45
Day closing