Computational challenges in bounded model checking - Clarke, E; Kroening, D; Ouaknine, J; Strichman, O (International Journal on Software Tools for Technology Transfer, 2005)