The problem addressed in this thesis is sound, scalable, demand-driven null-dereference verification for Java programs via over-approximated weakest preconditions analysis. The base version of this analysis having been ...