Exploring The Verification Corner

Recently, I was lucky enough to meet Rustan Leino whilst at a conference in Tallin, Estonia.  The Whiley project owes a lot to Rustan, as much of his work has been the inspiration behind Whiley.  In particular, his PhD thesis introduced the idea of Extended Static Checking and he then worked on the seminal ESC/Modula project,  which in turn became ESC/Java — the tool that widely popularised the idea.  He then worked on Spec# and is now working on Dafny.  All of these are programming systems which use compile-time verification of constraints (e.g. pre- and post-conditions), and have really set the standard for this field.

Anyhow, Rustan is a really interesting guy and we had a good chat about Whiley.  But, that’s not what I wanted to talk about here.  Rustan pointed me to his Verification Corner, which contains lots of interesting videos about verifying programs.  I’ve pulled out just a couple here that I liked, but there are otheres there … so go have a look around yourself!

Have fun!