A Foundation for Verifying Concurrent Programs (Lecture 0) - Leino, Rustan; Müller, Peter; Smans, Jan (FOSAD 2009, Bertinoro, Italy, 2009)
Program verification Prove program correctness for all possible inputs and behaviors