Using and Building an Automatic Program Verifier (Lecture 1) - Leino, Rustan (LASER Summer School 2011 Elba, Italy, 2011)
Functional correctness Limited checking