Introductory Lecture on Verification in Whiley

We’ve started using Whiley again in my second year course Formal Foundations of Programming. The aim of this course is to introduce students into a range of techniques related to software correctness. So far, we’ve looked at some static analysis and model checking tools.

Anyway, last week I gave an introductory lecture on writing specifications and verifying their implementations. Although this mostly focuses on some relatively simple examples, it should still be of interest to someone new to verification and/or Whiley: