Checker is well-known to uncover NPE and other things... was used in Guava, for instance.
http://types.cs.washington.edu/checker-framework/