Accurate Theorem Proving for Program Verification - Cook, B; Kroening, D; Sharygina, N (Proceedings of ISoLA 2004, 2006)