Nullness Analysis in Boolean Form

14 years 1 months ago
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 bytecode 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.
Fausto Spoto
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where SEFM
Authors Fausto Spoto
Comments (0)