Detecting inconsistencies via universal reachability analysis

11 years 7 months ago

Download users.soe.ucsc.edu

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-ﬁnding rather than veriﬁcation. 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 veriﬁcation technique, while in cases where some code is unknown, a theorem prover is incomplete, or speciﬁcations are incomplete, it can serve as bug ﬁnding technique with a low false-positive rate. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Veriﬁcation—Assertion checkers, programming by contract General Terms Veriﬁcation, Reliability, Languages Keywords Defect detection, weakest preconditions

Aaron Tomb, Cormac Flanagan

Real-time Traffic