Rustan on Automatic Program Verification

Yesterday I came across an interesting talk given by Rustan Leino at the University of Edinburgh in 2011.  Rustan takes an interesting look overview over the subject’s history, and then shows several tools in action (including Code Contracts and Dafny):

Anyway, Rustan has a long history in program verification now, and was heavily involved in the influential ESC/Java and Spec# verification tools, so definitely worth a look!