Dissertation/Thesis Abstract

Program inconsistency detection: Universal reachability analysis and conditional slicing
by Tomb, Aaron, Ph.D., University of California, Santa Cruz, 2011, 182; 3471818
Abstract (Summary)

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.

Indexing (document details)
Advisor: Flanagan, Cormac
School: University of California, Santa Cruz
School Location: United States -- California
Source: DAI-B 72/11, Dissertation Abstracts International
Subjects: Computer science
Keywords: Conditional slicing, Defect detection, Program analysis, Software verification
Publication Number: 3471818
ISBN: 9781124844589
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy