Null dereferences are a bane of programming in languages such as Java. In
this paper we propose a sound, demand-driven, inter-procedurally
context-sensitive dataflow analysis technique to verify a given dereference
as safe or potentially unsafe. Our analysis uses an abstract lattice of
formulas to find a pre-condition at the entry of the program such that a
null-dereference can occur only if the initial state of the program
satisfies this pre-condition.  We use a simplified domain of formulas,
abstracting out integer arithmetic, as well as unbounded access paths due
to recursive data structures. For the sake of precision we model aliasing
relationships explicitly in our abstract lattice, enable strong updates,
and use a limited notion of path sensitivity. For the sake of scalability
we prune formulas continually as they get propagated, reducing to {\tru}
conjuncts that are less likely to be useful in validating or invalidating
the formula. We have implemented our approach, and present an evaluation of
it on a set of ten real Java programs. Our results show that the set of
design features we have incorporated enable the analysis to (a) explore
long, inter-procedural paths to verify each dereference, with (b)
reasonable accuracy, and (c) very quick response time per dereference,
making it suitable for use in desktop development environments.