Nullness Analysis in Boolean Form

Attempts to dereference null result in an exception or a segmentation fault. Hence it is important to know those program points where this might occur and prove the others (or the entire program) safe. Nullness analysis of computer programs checks or infers non-null annotations for variables and object fields. Most nullness analyses currently use run-time checks or are incorrect or only verify manual annotations. We use here abstract interpretation to build and prove correct a static nullness analysis for Java byte code which infers non-null annotations. It is based on Boolean formulas, implemented with binary decision diagrams. Our experiments show it faster and more precise than the correct nullness analysis by Hubert, Jensen and Pichardie. We deal with static fields and exceptions, which is not the case of most other analyses. We claim that the result is theoretically clean and the implementation strong and scalable.