Computational challenges in bounded model checking
We describe several observations regarding the completeness and the complexity of bounded model checking and propose techniques to solve some of the associated computational challenges. We begin by defining the completeness threshold, we prove that the complexity of standard SAT-based BMC is doubly...
| Glavni autori: | , , , |
|---|---|
| Format: | Journal article |
| Izdano: |
Springer
2005
|
| _version_ | 1826274720098549760 |
|---|---|
| author | Clarke, E Kroening, D Ouaknine, J Strichman, O |
| author_facet | Clarke, E Kroening, D Ouaknine, J Strichman, O |
| author_sort | Clarke, E |
| collection | OXFORD |
| description | We describe several observations regarding the completeness and the complexity of bounded model checking and propose techniques to solve some of the associated computational challenges. We begin by defining the completeness threshold, we prove that the complexity of standard SAT-based BMC is doubly exponential and that, consequently, there is a complexity gap of an exponent between this procedure and standard LTL model checking. We discuss ways to bridge this gap. |
| first_indexed | 2024-03-06T22:47:45Z |
| format | Journal article |
| id | oxford-uuid:5dc3efc5-6a62-4245-aef6-aa94ab7a871a |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:47:45Z |
| publishDate | 2005 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:5dc3efc5-6a62-4245-aef6-aa94ab7a871a2022-03-26T17:36:21ZComputational challenges in bounded model checkingJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:5dc3efc5-6a62-4245-aef6-aa94ab7a871aSymplectic Elements at OxfordSpringer2005Clarke, EKroening, DOuaknine, JStrichman, OWe describe several observations regarding the completeness and the complexity of bounded model checking and propose techniques to solve some of the associated computational challenges. We begin by defining the completeness threshold, we prove that the complexity of standard SAT-based BMC is doubly exponential and that, consequently, there is a complexity gap of an exponent between this procedure and standard LTL model checking. We discuss ways to bridge this gap. |
| spellingShingle | Clarke, E Kroening, D Ouaknine, J Strichman, O Computational challenges in bounded model checking |
| title | Computational challenges in bounded model checking |
| title_full | Computational challenges in bounded model checking |
| title_fullStr | Computational challenges in bounded model checking |
| title_full_unstemmed | Computational challenges in bounded model checking |
| title_short | Computational challenges in bounded model checking |
| title_sort | computational challenges in bounded model checking |
| work_keys_str_mv | AT clarkee computationalchallengesinboundedmodelchecking AT kroeningd computationalchallengesinboundedmodelchecking AT ouakninej computationalchallengesinboundedmodelchecking AT strichmano computationalchallengesinboundedmodelchecking |