Speaker/Affiliation: Christo

ph Csallner/Georgia Institute of Technology

Date/Time: Thursday Ma

rch 20 2008 11:00 a.m.

Location: ACES 2.302

Host: William
Cook

Talk Title: Combining Static and Dynamic Analyses for Automat

ed Bug-Finding

Talk Abstract:
Finding bugs is like finding a few

needles in an infinitely
large haystack of program execution paths. Fals

e bug
warnings are one of the biggest problems both for
automated

correctness provers (such as type systems
and model-checkers) and for a

utomated bug-finders
(such as static bug-pattern matchers). To address
this
problem I will present three techniques for turning an
exis

ting powerful but false-positive-ridden static analysis
into a preci

se tool for automatic bug-finding.

First we will automatically conv

ert the output of a static
analysis to concrete JUnit test cases using

constraint
solving techniques. We thereby eliminate language-level
false bug warnings and make the results easier to understand
for human
consumers. We will then add a dynamic invariant
inference step to als

o address the harder problem of bug
warnings that are technically corre

ct but still irrelevant to the
user (these bugs could occur but only u

nder obscure conditions).
Finally we will adapt dynamic invariant infe

rence to work correctly
with subtyping. Previous approaches do not take
behavioral
subtyping into account and therefore produce imprecise or
inconsistent results which can throw off automated analyses
such as th

e ones we are performing for bug-finding.
I have implemented these techn

iques in the JCrasher Check ''n''
Crash and DSD-Crasher automatic test