Accurate Theorem Proving for Program Verification - Cook, B; Kroening, D; Sharygina, N (Springer, 2006)