Dr. David J. Pearce
Blog
Projects
Publications
Talks
Home
A Story of Cast Expressions
Friday, September 5th, 2014
Issue #427 “Bug with Dereferencing Array Types” seemed like just another bug. Submitted by a user last week (@Matt–), I didn’t think too much of it. But, as sometimes happens, appearances can be deceiving.
Read More…
Loop Variant Relations
Thursday, July 10th, 2014
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.
Read More…
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.
Read More…
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.
Read More…
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.
Read More…
Flying the CrazyFlie Quadcopter!
Sunday, March 2nd, 2014
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.
Read More…
More Tracked Arduino Fun!
Friday, January 31st, 2014
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.
Read More…
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.
Read More…
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.
Read More…
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.
Read More…
««
«
3
4
5
6
7
»
»»