Issues related to the dereferencing of null pointers are a pervasive and widely studied problem, and numerous static analyses have been proposed for this purpose. These are typically based on dataflow analysis, and take advantage of annotations indicating whether a type is nullable or not. The presence of such annotations can significantly improve the accuracy of null checkers. However, most code found in the wild is not annotated, and tools must fall back on default assumptions, leading to both false positives and false negatives. Manually annotating code is a laborious task and requires deep knowledge of how a program interacts with clients and components.

We propose to infer nullable annotations from an analysis of existing test cases. For this purpose, we execute instrumented tests and capture nullable API interactions. Those recorded interactions are then refined (santitised and propagated) in order to improve their precision and recall. We evaluate our approach on seven projects from the spring ecosystems and two google projects which have been extensively manually annotated with thousands of \texttt{@Nullable} annotations. We find that our approach has a high precision, and can find around half of the existing \texttt{@Nullable} annotations. This suggests that the method proposed is useful to mechanise a significant part of the very labour-intensive annotation task.

Fri 21 Jul

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
ECOOP 7: Verification and TestingResearch Papers at Amazon Auditorium (Gates G20)
Chair(s): Wenxi Wang University of Texas at Austin
10:30
15m
Talk
On using VeriFast, VerCors, Plural, and KeY to check object usage
Research Papers
João Mota NOVA School of Science and Technology, António Ravara NOVA LINCS & FCT, NOVA University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
DOI
10:45
15m
Talk
Exact Separation Logic
Research Papers
Petar Maksimović Imperial College London, UK, Caroline Cronjäger Ruhr-Universität Bochum, Andreas Lööw Imperial College London, Julian Sutherland Imperial College London, Philippa Gardner Imperial College London
DOI Pre-print
11:00
15m
Talk
Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs
Research Papers
Ashish Mishra Purdue University, Suresh Jagannathan Purdue University
DOI
11:15
15m
Talk
Constraint Based Compiler Optimization for Energy Harvesting Applications
Research Papers
Yannan Li University of Southern California, Chao Wang University of Southern California
DOI
11:30
15m
Talk
Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises
Research Papers
Feiyang Jin Georgia Institute of Technology, Lechen Yu Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology
DOI
11:45
15m
Talk
On Leveraging Tests to Infer Nullable Annotations
Research Papers
Jens Dietrich Victoria University of Wellington, David J. Pearce ConsenSys, Mahin Chandramohan Oracle Labs
DOI