Record Details

Improving the Precision of a Scalable Demand-Driven Null- Dereference Verification for Java

Electronic Theses of Indian Institute of Science

View Archive Info
 
 
Field Value
 
Title Improving the Precision of a Scalable Demand-Driven Null- Dereference Verification for Java
 
Creator Margoor, Amogh
 
Subject Java (Computer Programme Language)
Java Programs - Verification
Java Collections
Java Maps
Java Programs - Base Analysis
Computer Programs - Verification
Java Container Class Methods
Computer Science
 
Description The problem addressed in this thesis is sound, scalable, demand-driven null-dereference verification for Java programs via over-approximated weakest preconditions analysis. The base version of this analysis having been described in a previous publication, in this thesis we focus primarily on describing two major optimizations that we have incorporated that allow for longer program paths to be traversed more efficiently, hence increasing the precision of the approach. The first optimization is to bypass certain expensive-to-analyze constructs, such as virtual calls with too many possible targets, by directly transferring dataflow facts from points after the construct to points before along def-use edges of a certain kind. The second optimization is to use manually constructed summaries of Java container class methods, rather than analyze the code of these methods directly. We evaluate our approach using 10 real world Java programs, as well as several micro benchmarks. We demonstrate that our optimizations result in a 45% reduction in false positives over the base version on the real programs, without significant impact on running time.
 
Contributor Rasghavan, K V
 
Date 2018-03-19T08:05:04Z
2018-03-19T08:05:04Z
2018-03-19
2013
 
Type Thesis
 
Identifier http://hdl.handle.net/2005/3284
http://etd.ncsi.iisc.ernet.in/abstracts/4146/G25614-Abs.pdf
 
Language en_US
 
Relation G25614