Computing over-approximations with bounded model checking
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 th...
| Main Author: | |
|---|---|
| Format: | Journal article |
| Published: |
Elsevier
2006
|
| _version_ | 1826290757181374464 |
|---|---|
| author | Kroening, D |
| author_facet | Kroening, D |
| author_sort | Kroening, D |
| collection | OXFORD |
| description | 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 designs for better verification and testing results. This paper presents an automated technique based on cut-point insertion to obtain an over-approximation of the model that 1) preserves safety properties and 2) has a which is small enough to actually prove ϕ using BMC. The algorithm uses proof-based abstraction refinement to remove spurious counterexamples. |
| first_indexed | 2024-03-07T02:49:04Z |
| format | Journal article |
| id | oxford-uuid:ad0bf6c7-644e-4f07-99bb-cde1c781abe4 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:49:04Z |
| publishDate | 2006 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:ad0bf6c7-644e-4f07-99bb-cde1c781abe42022-03-27T03:32:57ZComputing over-approximations with bounded model checkingJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:ad0bf6c7-644e-4f07-99bb-cde1c781abe4Symplectic Elements at OxfordElsevier2006Kroening, DBounded 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 designs for better verification and testing results. This paper presents an automated technique based on cut-point insertion to obtain an over-approximation of the model that 1) preserves safety properties and 2) has a which is small enough to actually prove ϕ using BMC. The algorithm uses proof-based abstraction refinement to remove spurious counterexamples. |
| spellingShingle | Kroening, D Computing over-approximations with bounded model checking |
| title | Computing over-approximations with bounded model checking |
| title_full | Computing over-approximations with bounded model checking |
| title_fullStr | Computing over-approximations with bounded model checking |
| title_full_unstemmed | Computing over-approximations with bounded model checking |
| title_short | Computing over-approximations with bounded model checking |
| title_sort | computing over approximations with bounded model checking |
| work_keys_str_mv | AT kroeningd computingoverapproximationswithboundedmodelchecking |