Journal article

Computational challenges in bounded model checking

Abstract:: 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.

Publication status:: Published

Peer review status:: Peer reviewed

Actions

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Cite

Cite this record

APA Style

Clarke, E., Kroening, D., Ouaknine, J., & Strichman, O. (2005). Computational challenges in bounded model checking. International Journal on Software Tools for Technology Transfer, 7(2), 174–183.

MLA Style

Clarke, E., et al. “Computational Challenges in Bounded Model Checking.” International Journal on Software Tools for Technology Transfer, vol. 7, no. 2, Springer, 2005, pp. 174–83.

Chicago Style

Clarke, E, D Kroening, J Ouaknine, and O Strichman. 2005. “Computational Challenges in Bounded Model Checking.” International Journal on Software Tools for Technology Transfer 7 (2): 174–83.
Share
Print

Access Document

Publisher copy:: 10.1007/s10009-004-0182-5

Authors

+ Clarke, E More by this author

Role:: Author

+ Kroening, D More by this author

Institution:: University of Oxford
Division:: MPLS
Department:: Computer Science
Role:: Author

+ Ouaknine, J More by this author

Role:: Author

+ Strichman, O More by this author

Role:: Author

Publisher:: Springer
Journal:: International Journal on Software Tools for Technology Transfer More from this journal
Volume:: 7
Issue:: 2
Pages:: 174-183
Publication date:: 2005-02-15
DOI:: 10.1007/s10009-004-0182-5
EISSN:: 1433-2787
ISSN:: 1433-2779

Keywords:: SBTMR
Pubs id:: pubs:282315
UUID:: uuid:5dc3efc5-6a62-4245-aef6-aa94ab7a871a
Local pid:: pubs:282315
Source identifiers:: 282315
Deposit date:: 2017-01-28

Terms of use

Copyright holder:: Springer
Copyright date:: 2005
Notes:: © Springer-Verlag 2005

Licence:: Terms and Conditions of Use for Oxford University Research Archive

Views and Downloads

About 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