Print Email Facebook Twitter Provably Sound Nullness Analysis of Java Code Title Provably Sound Nullness Analysis of Java Code Author Raateland, Wouter (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Keidel, Sven (mentor) Erdweg, Sebastian (mentor) Degree granting institution Delft University of Technology Project sturdy Date 2018-07-03 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. Subject Static AnalysisAbstract InterpretationNullness AnalysisJavaArrows To reference this document use: http://resolver.tudelft.nl/uuid:f700b5fa-286b-42b0-b397-fa28dea2977f Part of collection Student theses Document type bachelor thesis Rights © 2018 Wouter Raateland Files PDF Provably_Sound_Nullness_A ... a_Code.pdf 264.68 KB Close viewer /islandora/object/uuid:f700b5fa-286b-42b0-b397-fa28dea2977f/datastream/OBJ/view