Exploiting Structure for Scalable Software Verification
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@phdthesis{babic08,
author = {Domagoj Babi\'c},
title = {{Exploiting Structure for Scalable Software Verification}},
school = {University of British Columbia, Vancouver, Canada},
year = {2008},
}
Abstract:
Software bugs are expensive. Recent estimates by the US National
Institute of Standards and Technology claim that the cost of software
bugs to the US economy alone is approximately 60 billion USD annually.
As society becomes increasingly software-dependent, bugs also reduce
our productivity and threaten our safety and security. Decreasing
these direct and indirect costs represents a significant research
challenge as well as an opportunity for businesses.
Automatic software bug-finding and verification tools have a
potential to completely revolutionize the software engineering industry
by improving reliability and decreasing development costs. Since
software analysis is in general undecidable, automatic tools have to
use various abstractions to make the analysis computationally tractable.
Abstraction is a double-edged sword: coarse abstractions, in general,
yield easier verification, but also less precise results.
This thesis focuses on exploiting the structure of software for
abstracting away irrelevant behavior. Programmers tend to organize
code into objects and functions, which effectively represent natural
abstraction boundaries. Humans use such structural abstractions to
simplify their mental models of software and for constructing informal
explanations of why a piece of code should work. A natural question
to ask is: How can automatic bug-finding tools exploit the same
natural abstractions? This thesis offers possible answers.
More specifically, I present three novel ways to exploit
structure at three different steps of the software analysis process.
First, I show how symbolic execution can preserve the data-flow
dependencies of the original code while constructing compact
symbolic representations of programs. Second, I propose structural abstraction,
which exploits the structure preserved by the symbolic
execution. Structural abstraction solves a long-standing open problem
--- scalable interprocedural path- and context-sensitive program
analysis. Finally, I present an automatic tuning approach that
exploits the fine-grained structural properties of software (namely,
data- and control-dependency) for faster property checking. This
novel approach resulted in a 500-fold speedup over the best previous
techniques. Automatic tuning not only redefined the limits of
automatic software analysis tools, but also has already found its
way into other domains (like model checking), demonstrating the
generality and applicability of this idea.