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

• Type: Journal
• Year: 2012
• Where: ISSTA
• Authors: Aaron Tomb, Cormac Flanagan
• Keywords: Inconsistency Detection, ISSTA 2012, Precondition Calculus, Software Engineering, Theorem Prover