Semantic Foundations and Inference of Non-null Annotations

This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in objectoriented programs. The analysis is formulated for a minimalistic OO and is expressed as a constraint-based abstract interpretation of the program which for each field of a class infers whether the field is definitely non-null or possibly null after object initialization. The analysis is proved correct with respect to an operational semantics of the minimalistic OO language. This correctness proof has been machine checked using the Coq proof assistant. We also prove the analysis complete with respect to the non-null type system proposed by F

• Type: Conference
• Year: 2008
• Where: FMOODS
• Authors: Laurent Hubert, Thomas P. Jensen, David Pichardie
• Keywords: Analysis, FMOODS 2008, Formal Methods, Minimalistic Oo, Null Pointer Analysis