Software inevitably contains mistakes and operates incorrectly in at least some situations. As a result, many techniques and tools have arisen to detect problems in software. However, these techniques have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior—often a collection of independent assertions sprinkled throughout the program.
Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bug-finding rather than verification. In this dissertation, we describe an inconsistency detection analysis that extends previous work and is based on the foundation of the weakest precondition calculus. In the ideal case (a completely closed program and a perfect theorems prover), this analysis can serve as a full safety verification technique, while in realistic cases (where some code is unknown and theorem provers are incomplete) it can serve as bug finding technique with a low false-positive rate. It smooths the path from bug-finding to verification by using the same base analysis for both goals.
Our analysis detects inconsistencies that come as violations of a property we call universal reachability. These violations can range from serious crash-causing bugs or security vulnerabilities to dead code, but usually indicate problems that should be fixed. We have applied our analysis to a large body of widely-used open-source software, and found a number of bugs, with few false positives.
|School:||University of California, Santa Cruz|
|School Location:||United States -- California|
|Source:||DAI-B 72/11, Dissertation Abstracts International|
|Keywords:||Conditional slicing, Defect detection, Program analysis, Software verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be