Journal article icon

Journal article

Linear Completeness Thresholds for Bounded Model Checking.

Abstract:

Bounded model checking is a symbolic bug-finding method that examines paths of bounded length for violations of a given LTL formula. Its rapid adoption in industry owes much to advances in SAT technology over the past 10-15 years. More recently, there have been increasing efforts to apply SAT-based methods to unbounded model checking. One such approach is based on computing a completeness threshold: a bound k such that, if no counterexample of length k or less to a given LTL formula is found,...

Expand abstract

Actions


Access Document


Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author

Contributors

Role:
Editor
Publisher:
Springer Publisher's website
Journal:
CAV
Volume:
6806
Pages:
557-572
Publication date:
2011-01-01
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
Language:
English
Pubs id:
pubs:304706
UUID:
uuid:685726ae-19f7-4c9a-a0db-3d08472f6c35
Local pid:
pubs:304706
Source identifiers:
304706
Deposit date:
2012-12-19

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP