Provably Sound Nullness Analysis of Java Code

Bachelor Thesis (2018)
Author(s)

W. Raateland (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Contributor(s)

S. Keidel – Mentor

S.T. Erdweg – Mentor

Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright
© 2018 Wouter Raateland
More Info
expand_more
Publication Year
2018
Language
English
Copyright
© 2018 Wouter Raateland
Graduation Date
03-07-2018
Awarding Institution
Delft University of Technology
Project
sturdy
Faculty
Electrical Engineering, Mathematics and Computer Science
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.

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.

Files

License info not available