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 (Cτ problem: for every finite model M and an LTL property there ex...

Full description

Bibliographic Details
Main Authors: Clarke, E, Kroening, D, Ouaknine, J, Strichman, O
Format: Journal article
Language:English
Published: 2005