Detecting inconsistencies via universal reachability analysis

8 years 5 months ago
Detecting inconsistencies via universal reachability analysis
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. We describe an inconsistency detection analysis that extends previous work and is based on the foundation of the weakest precondition calculus. On a closed program, this analysis can serve as a full verification technique, while in cases where some code is unknown, a theorem prover is incomplete, or specifications are incomplete, it can serve as bug finding technique with a low false-positive rate. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification—Assertion checkers, programming by contract General Terms Verification, Reliability, Languages Keywords Defect detection, weakest preconditions
Aaron Tomb, Cormac Flanagan
Added 28 Sep 2012
Updated 28 Sep 2012
Type Journal
Year 2012
Authors Aaron Tomb, Cormac Flanagan
Comments (0)