Articles

Testing out my Papilio FPGA!

Recently, I got hold of a Papilio One (which you can think of as the Arduino of FPGAs).  The Papilio board has a Xilinx Spartan 3 on board, which is plenty enough to get started learning about FPGAs.  Here’s what the board looks like:

Now, it might look big above … . . . → Read More: Testing out my Papilio FPGA!

Building an Arduino Robot (for Testing Whiley)

The Whiley programming language is about developing more reliable software and, of course, embedded systems is one of the biggest areas that could benefit. Obviously, then, we need an “embedded system” to test Whiley with, right?  At least, that’s the thinking behind my recent endeavor to create an Arduino-based Robot.

After some discussion with our workshop . . . → Read More: Building an Arduino Robot (for Testing Whiley)

A Source File with 72KLOC!?

Yesterday, I was looking at the stats on Ohloh for the Whiley project and noticed that my total line count for the project had increased from around 65KLOCto 143KLOC over a very short amount of time:

Confused, I was pondering this for a while.  Then it struck me: I’d checked in . . . → Read More: A Source File with 72KLOC!?

Whiley v0.3.17 Released!

Whilst it’s been over three months since the last release of Whiley, this latest release is chocked full of improvements!  I’ve closed around 60 issues in that time, and have completely reworked the theorem prover from scratch.  This means compile-time checking of constraints is starting to work better — however, there remains quite a . . . → Read More: Whiley v0.3.17 Released!

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