[pl-seminar] REMINDER: PL talk tomorrow at 4pm room 4310

[Susan Horwitz <horwitz@xxxxxxxxxxx>]

Demand driven inter-procedural null-dereference verification
Raghavan Komondoor
IISc Bangalore
Tuesday, November 01, 2011
4:00 PM, 4310 CS

Null dereferences are a bane of programming in languages such as Java. 
In this talk we propose a sound, demand-driven, inter-procedurally 
context-sensitive dataflow analysis technique to verify a given 
dereference as safe or potentially unsafe. Our analysis uses an abstract 
lattice of formulas to find a pre-condition at the entry of the program 
such that a null-dereference can occur only if the initial state of the 
program satisfies this pre-condition.
We use a simplified domain of formulas, abstracting out integer 
arithmetic as well as unbounded access paths. For the sake of precision 
we model aliasing relationships explicitly in our abstract lattice, 
enable strong updates, and use a limited notion of path sensitivity.
We have implemented our approach, and present an evaluation of it on a 
set of ten real Java programs. Our results show that the set of design 
features we have incorporated enable the analysis to (a) explore long, 
inter-procedural paths to verify each dereference, with (b) reasonable 
accuracy, and (c) very quick response time per dereference.