Verifying Dereference Safety Via Expanding-Scope Analysis

This paper addresses the challenging problem of verifying the safety of pointer dereferences in real Java programs. The paper provides an automatic approach to this problem based on a sound interprocedural analysis. The paper presents a staged expanding-scope algorithm for interprocedural abstract interpretation, which invokes sound analysis with partial programs of increasing scope. This algorithm achieves many benefits typical of whole-program interprocedural analysis, but scales to large programs by limiting analysis to small program fragments. To address cases where the static analysis of program fragments fails to prove safety, the analysis also suggests possible annotations which, if a user accepts, ensure the desired properties.