Talk Title: Symbolic Analysis for Java
<

br>Talk Abstract:
Bug-finding tools that are based on approximate analys

is
often report false positives. Burned enough by false positives

a skeptical programmer wants to see convincing evidence that
a bug repo

rt is indeed feasible. Symbolic analysis can often help
produce such ev

idence in the form of a concrete test case that
can reproduce a feasibl

e bug.

In this talk I will describe our recent work on symbolic ana

lysis
of Java programs. Our main technical contribution is in the handl

ing
of procedure calls during symbolic analysis. We present new
te

chniques to make symbolic analysis work effectively on realistic
Java a

pplications without requiring hand-written specifications of
procedure

s and without inlining procedure calls away. I will present
our preli

minary experience with building a bug validator based on
symbolic analy

sis and discuss some open issues.

This talk is based on joint work

with Stephen Fink and Manu Sridharan
both of IBM Research.

Spea

ker Bio:
Satish Chandra obtained a PhD from the University of Wisconsin-

Madison in 1997 and a B.Tech from the Indian Institute of Technology-Kanpur in 1991 both in computer science. From 1997 to 2002 he was