Journal article icon

Journal article

Computing over-approximations with bounded model checking

Abstract:

Bounded Model Checking (BMC) searches for counterexamples to a property ϕ with a bounded length k. If no such counterexample is found, k is increased. This process terminates when k exceeds the completeness threshold (i.e., k is sufficiently large to ensure that no counterexample exists) or when the SAT procedure exceeds its time or memory bounds. However, the completeness threshold is too large for most practical instances or too hard to compute. Hardware designers often modify their desig...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's version

Actions


Access Document


Files:
Publisher copy:
10.1016/j.entcs.2005.07.021

Authors


More by this author
Department:
Oxford, MPLS, Computer Science
Publisher:
Elsevier Publisher's website
Journal:
Electronic Notes in Theoretical Computer Science Journal website
Volume:
144
Issue:
1
Pages:
79-92
Publication date:
2006-01-06
DOI:
EISSN:
1571-0661
Pubs id:
pubs:327183
URN:
uri:ad0bf6c7-644e-4f07-99bb-cde1c781abe4
UUID:
uuid:ad0bf6c7-644e-4f07-99bb-cde1c781abe4
Local pid:
pubs:327183

Terms of use


Metrics



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

TO TOP