Verifying Software with Whiley

A couple of weeks back, I gave a presentation to the Wellington Java User Group. The talk provides a useful introduction to verifying software in Whiley, and shows a bunch of interesting examples. Anyway, you can see the presentation here:

Wellington Java User Group Presentation from John Hurst on Vimeo.

. . . → Read More: Verifying Software with Whiley

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 . . . → Read More: Introductory Lecture on Verification in Whiley

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.

At first, I had a lot of problems trying to fly it.  After a lot of fairly major . . . → Read More: Flying the CrazyFlie Quadcopter!

More Tracked Arduino Fun!

Recently, I’ve been upgrading my tracked arduino robot with a few more sensors. Check out the video:

The robot has two medium range IR sensors (front and back), as well as a downward facing short-range IR sensor. When the front sensor detects something is very close, the robot backs up (provided the back . . . → Read More: More Tracked Arduino Fun!

Whiley at the Melbourne Java User Group

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. Well, here’s the talk …

You can also get the slides from here!

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

Rustan on Automatic Program Verification

Yesterday I came across an interesting talk given by Rustan Leino at the University of Edinburgh in 2011.  Rustan takes an interesting look overview over the subject’s history, and then shows several tools in action (including Code Contracts and Dafny): Anyway, Rustan has a long history in program verification now, and was heavily involved . . . → Read More: Rustan on Automatic Program Verification

Autonomous Robotic Drone which Flies Indoors!?

Very recently, I came across this article from MIT News about an autonomous robotic drone developed at MIT.  It’s incredibly neat stuff … and I would love to get Whiley running on something like this!  Here’s the video from the article:

Anyhow, one day I will build one of these things . . . → Read More: Autonomous Robotic Drone which Flies Indoors!?

Exploring The Verification Corner

Recently, I was lucky enough to meet Rustan Leino whilst at a conference in Tallin, Estonia.  The Whiley project owes a lot to Rustan, as much of his work has been the inspiration behind Whiley.  In particular, his PhD thesis introduced the idea of Extended Static Checking and he then worked on the seminal . . . → Read More: Exploring The Verification Corner

Connecting the Dots on the Future of Programming Languages

Yesterday, I serendipitously came across two things which got me thinking about the future of programming languages:

The first was an excellent article entitled “Welcome to the Hardware Jungle” by Herb Sutter. This article is about the coming advent our multicore overlords. Whilst this might sound like something you’ve heard before, it’s actually well . . . → Read More: Connecting the Dots on the Future of Programming Languages