Nullness Analysis in Boolean Form

Attempts to dereference nil result in anexception or a segmentation fault. Hence itis importantto know those program points where this might occur and provethe others (or the entire program) safe.Nullness analysis of computer programs checks or infers non-nil annotationsfor variables and object fields. Most nullnessanalyses currently use run-time checks or are incorrect or only verifymanual annotations. We use here abstract interpretationto build and prove correct a static nullness analysis for Javabytecode which infers non-nil annotations. It isbased on Boolean formulas, implemented with binary decisiondiagrams. Our experiments show it faster and more precise than the correctnullness analysis by Hubert, Jensen and Pichardie.We deal with static fields and exceptions, which isnot the case of most other analyses. We claim that the result istheoretically clean and the implementation strong and scalable.