The Dafny Tutorial at SPLASH'13

Today I was attending the Dafny tutorial given by Rustan Leino at SPLASH'13. I have to say that this was the highlight of the conference for me. In case you haven’t come across it before, Dafny is a programming language designed for software verification.

The Architecture of Verification in Whiley

As the Whiley compiler continues to evolve, certain aspects of its architecture are really starting to mature. One of the more recent pieces to take shape is the verification pipeline. This is the process by which a Whiley file is converted into a series of verification conditions, which are then checked by the automated theorem prover.

Input / Output and the Object-Oriented Paradigm

Today, more then ever before, I/O dominates what software is about. Of course, it’s always been important but, with increasing bandwidths, I/O seems to be what most programs now spend most of their time doing.

Compile-Time Verification and I/O

A surprisingly common question people ask me when I talk about compile-time checking of pre-/post-conditions and invariants is: how do you deal with I/O? To understand what the difficulty is, let’s consider a simple example in Whiley:

Whiley Puzzler

I was having an interesting discussion with a colleague today about various aspects of Whiley, and we came up with an interesting bit of example code which is something of a puzzler.