Articles

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. It has a lot in common with . . . → Read More: The Dafny Tutorial at SPLASH’13

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 . . . → Read More: The Architecture of Verification in Whiley

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:

define nat as int where $ >= 0 define pos as int where $ > 0 define . . . → Read More: Compile-Time Verification and I/O

Understanding Loop Invariants in Whiley

In this article, I’ll look at a common problem one encounters when verifying programs: namely, writing loop invariants.  In short, a loop invariant is a property of the loop which:

holds on entry to the loop; holds after the loop body is executed; holds when the loop finishes.

Loop invariants can be tricky to . . . → Read More: Understanding Loop Invariants in Whiley

Generating Verification Conditions for Whiley

Probably the most interesting aspect of the Whiley language is that it supports compile-time verification of preconditions, postconditions and other invariants.  There are two main aspects of how this works:

Generation of Verification Conditions (VCs) from the source code.  A verification condition is a logical expression which, if proved to be satisfiable, indicates an . . . → Read More: Generating Verification Conditions for Whiley

Illustrating Compile-Time Verification in Whiley

With the latest release of Whiley, compile-time checking of constraints can be enabled with a command-line switch.  So, I thought a few examples of this were in order.

Example: Absolute of an Integer

Consider this simple program:

define nat as int where $ >= 0 nat abs(int x): return x

This defines a type . . . → Read More: Illustrating Compile-Time Verification in Whiley

A Problem on Typing vs Verification

Whiley uses a flow-sensitive type system, and a verification engine to enable [[Extended static checking]]. My desire in designing these two subsystems is to keep them completely isolated. In particular, such that we can always compile and run a Whiley program with verification turned off. This requirement stems from the fact that verification of . . . → Read More: A Problem on Typing vs Verification