Output details
11 - Computer Science and Informatics
University of Oxford
Return to search
Output 0 of 0 in the submission
Output title
On the Magnitude of Completeness Thresholds in Bounded Model Checking
Type
E - Conference contribution
Name of conference/published proceedings
2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS)
Volume number
-
Issue number
-
First page of article
155
ISSN of proceedings
1043-6871
Year of publication
2012
Number of additional authors
3
Additional information
<10>
Bounded model checking (BMC) is described by Ed Clarke in his Turing Award lecture as "probably the most widely used model checking technique". BMC is typically used as a bug-finding technique, and Clarke proceeds to ask whether it can also be used prove correctness. This paper addresses the problem, giving an algorithm that determines whether a given specification has a "completeness threshold" (the depth one must search to certify correctness) linear in the diameter of the model. This greatly generalises previous work of Bierre, Clarke and others, which only identified particular specifications with linear completeness thresholds.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
