``Combining over- and under-approximating program analyses for automatic software testing''
by Christoph Csallner.
Ph.D. dissertation, Georgia Tech, Aug. 2008.
Abstract
This dissertation attacks the well-known problem of path-imprecision in
static program analysis. Our starting point is an existing static program
analysis that over-approximates the execution paths of the analyzed
program. We then make this over-approximating program analysis more
precise for automatic testing in an object-oriented programming language.
We achieve this by combining the over-approximating program analysis with
usage-observing and under-approximating analyses. More specifically, we
make the following contributions. We present a technique to eliminate
language-level unsound bug warnings produced by an
execution-path-over-approximating analysis for object-oriented programs
that is based on the weakest precondition calculus. Our technique
post-processes the results of the over-approximating analysis by solving
the produced constraint systems and generating and executing concrete
test-cases that satisfy the given constraint systems. Only test-cases that
confirm the results of the over-approximating static analysis are
presented to the user. This technique has the important side-benefit of
making the results of a weakest-precondition based static analysis easier
to understand for human consumers. We show examples from our experiments
that visually demonstrate the difference between hundreds of complicated
constraints and a simple corresponding JUnit test-case. Besides
eliminating language-level unsound bug warnings, we present an additional
technique that also addresses user-level unsound bug warnings. This
technique pre-processes the testee with a dynamic analysis that takes
advantage of actual user data. It annotates the testee with the knowledge
obtained from this pre-processing step and thereby provides guidance for
the over-approximating analysis. We also present an improvement to dynamic
invariant detection for object-oriented programming languages. Previous
approaches do not take behavioral subtyping into account and therefore may
produce inconsistent results, which can throw off automated analyses such
as the ones we are performing for bug-finding. Finally, we address the
problem of unwanted dependencies between test-cases caused by global
state. We present two techniques for efficiently re-initializing global
state between test-case executions and discuss their trade-offs. We have
implemented the above techniques in the JCrasher, Check 'n' Crash, and
DSD-Crasher tools and present initial experience in using them for
automated bug finding in real-world Java programs.
@phdthesis{csallner08combining,
author = {Christoph Csallner},
title = {Combining over- and under-approximating program analyses for
automatic software testing},
school = {Georgia Tech},
type = {{Ph.D.}},
month = aug,
year = {2008}
}
Copyright notice:
This material is presented to ensure timely dissemination of scholarly and
technical work. Copyright and all rights therein are retained by authors or
by other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each author s
copyright. In most cases, these works may not be reposted without the
explicit permission of the copyright holder.