Computational challenges in bounded model checking. - Clarke, E; Kroening, D; Ouaknine, J; Strichman, O (STTT, 2005)