Provably Sound Nullness Analysis of Java Code

Bachelor thesis (2018)

Authors

W. Raateland Electrical Engineering, Mathematics and Computer Science

Contributors

S. Keidel (mentor)
S.T. Erdweg (mentor)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2018 Wouter Raateland
More Info
expand_more

Published Date

03-07-2018

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Null pointer dereferences in Java raise exceptions, occur often, are hard to debug and cost a lot of unnecessary effort and resources. Therefore, a lot of effort has been put in analyses spotting those null pointer dereferences. As developers rely on those analyses it is important that they are sound. However, proving null pointer analyses sound has been a complex problem. Hence, we developed a nullness analysis for Java that is provably sound. The analysis is built as an abstract interpreter upon the sturdy framework, that allows for compositional soundness proofs. This reduces the proof effort greatly. By creating a concrete interpreter, and by generating arbitrary programs, we were able to assess the soundness of the nullness analysis to great extend. Also, we have proven a part of the analysis to be sound in a formal way.