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.

Verification with Data from Untrusted Sources

Recently, I was listening to the latest edition of the Illegal Argument podcast, and it turns out they were discussing Whiley! (about 103:16 minutes in). The discussion was about how verification interacts with data from an untrusted source (e.

Loop Variant Relations

Proving that a loop always terminates is a common requirement when verifying software. The usual approach to doing this is to provide a loop variant function. This is typically an integer expression which decreases on every iteration of the loop.

Loop Invariants and Do/While Statements

Recently, I encountered what I thought was a bug in the Whiley Compiler. The issue related to the current treatment of do/while loops and loop invariants. Having now spent a fair bit of time researching the issue, the answer is not so clear.

Flying the CrazyFlie Quadcopter!

Last week, my CrazyFlie nano-quadcopter finally arrived and, since then, I’ve been learning how to fly! The copter is much smaller than I was expecting, and it requires you to solder a few bits together.