Dr. David J. Pearce

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!