How Did Software Get So Reliable Without Proof?

Tony Hoare’s 1996 paper How Did Software Get So Reliable Without Proof? addresses the apparent paradox where software more or less works without having been either proved correct or tested on more than an infinitesimal fraction of its execution paths. Early in the paper we read: Dire warnings have been issued of the dangers of […]


I just got back from Tampere, Finland where I was one of the program chairs for EMSOFT, an embedded software conference. If I haven’t blogged about this much, it’s because I’m sort of a reluctant and not especially talented organizer of events. Happily, EMSOFT is just one third of the larger Embedded Systems Week, so […]

ARM Math Quirks on Raspberry Pi

Embedded processors can be relied upon to be a little quirky. Lately I’ve been playing around with the Raspberry Pi’s BCM2835 processor, which is based on the ARM1176JZF-S core. The “J” stands for Jazelle, a module that permits this processor to execute Java bytecodes directly. As far as I know there’s no open source support […]

High-Resolution Timing on the Raspberry Pi

Just to be clear, this post is about measuring the times at which events happen. Making things happen at specific times is a completely separate (and much harder) problem. The clock_gettime() function (under Raspbian) gives results with only microsecond resolution and also requires almost a microsecond to execute. This isn’t very helpful when trying to […]

Why Verify Software?

People like me who work on software verification (I’m using the term broadly to encompass static analysis, model checking, and traditional formal verification, among others) like to give talks where we show pictures of exploding rockets, stalled vehicles, inoperable robots, and crashed medical devices. We imply that our work is helping, or at least could […]