The problem addressed in this paper is sound, scalable, demand-driven
null-dereference verification for Java programs.  Our approach consists
conceptually of a base analysis, plus two major extensions for enhanced
precision. The base analysis is a dataflow analysis wherein we propagate
formulas in the backward direction from a given dereference, and compute a
necessary condition at the entry of the program for the dereference to be
potentially unsafe. The extensions are motivated by the presence of certain
"difficult" constructs in real programs, e.g., virtual calls with too
many candidate targets, and library method calls, which happen to need
excessive analysis time to be analyzed fully.  The base analysis is hence
configured to skip such a difficult construct when it is encountered by
dropping all information that has been tracked so far that could
potentially be affected by the construct.  Our extensions are essentially
more precise ways to account for the effect of these constructs on
information that is being tracked, without requiring full analysis of these
constructs.  The first extension is a novel scheme to transmit formulas
along certain kinds of def-use edges, while the second extension is based
on using manually constructed backward-direction summary functions of
library methods.  We have implemented our approach, and applied it on a set
of real-life benchmarks.  The base analysis is on average able to declare
about 84% of dereferences in each benchmark as safe, while the two
extensions push this number up to 91%.