Completeness and Complexity of Bounded Model Checking - Clarke, E; Kroening, D; Strichman, O; Ouaknine, J (2004)