David J. Pearce (Blog)

Understanding Ghost Variables in Software Verification

Friday, June 20th, 2014

Verification tools often support the use of ghost variables to help in the verification process. A ghost variable is not needed for the program to execute, and will not be compiled into object code.

Loop Invariants and Do/While Statements

Thursday, May 15th, 2014

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.

Loop invariants and Break Statements

Friday, May 2nd, 2014

In this article, I’ll look at some interesting issues relating to the use of break statements within loops, and how this affects the idea of a loop invariant. For some general background on writing loop invariants in Whiley, see my previous post.

Thoughts on Parsing Whiley (and Indentation Syntax)

Thursday, January 23rd, 2014

Recently, I have been reworking the Whiley compiler’s parser to make it more robust. Doing this has opened up some interesting issues, which I thought were worth discussing. Whiley uses indentation syntax without explicit end-of-statement terminators (e.

Thoughts on Writing Loop Invariants

Tuesday, November 19th, 2013

As the Whiley system is taking better shape every day, I’m starting to play around more and discover things. In particular, there are some surprising issues surrounding while loops and their loop invariants.

The Dafny Tutorial at SPLASH'13

Friday, November 1st, 2013

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.

Understanding why Union Types are useful

Wednesday, July 31st, 2013

The Whiley programming language uses union types as a way of combining types together. Here’s a simple example to illustrate: function indexOf(string str, char c) => null|int: for i in 0.

The Architecture of Verification in Whiley

Wednesday, June 26th, 2013

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.

Whiley at the Melbourne Java User Group

Wednesday, June 19th, 2013

A few weeks ago, I was in Melbourne attending the Australasian Software Engineering Conference and, whilst I was there, I gave a talk on Whiley at the Melbourne Java Users Group.

Input / Output and the Object-Oriented Paradigm

Thursday, May 16th, 2013

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.

2
3
4
5
6