Cogent: Accurate theorem proving for program verification - Cook, B; Kroening, D; Sharygina, N (Springer, 2005)