Nullness Analysis for Java

Google Tech Talks
September 17, 2008

ABSTRACT

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 simply syntactical (as in Eclipse and Idea) or incorrect or only verify manual annotations. We use 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. The result is theoretically clean and the implementation strong and scalable.

Speaker: Prof. Fausto Spoto
Fausto Spoto is associate professor at the University of Verona, Italy. He took a PhD in computer science from the University of Pisa, where he started working at the static analysis of computer programs. His current interests are related to the analysis of Java and Java bytecode programs.

He wrote a tool, Julia, which analyzes Java bytecode programs by using abstract interpretation and presents the results to the user, for verification as well as for code optimisation.