Category Archives: Uncategorized

Think you know C? Think again…

There’s a great article in the latest issue of ACM Queue about the effects of uninitialized variables in C by Robert Seacord.  See here

Robert is a noted expert and was the principal author of the CERT C Coding Standard, so he really does know what he’s on about.  The good news: the article is the most complete and up-to-date treatment of this topic that I know of – I certainly learned lots from it, especially with regard to what C’11 has to say.  The bad news: it’s worse, much worse, than you think…

Question: would it be possible to define a subset of C which is both useful and guarantees sound data-flow analysis in P-Time? I fear the answer is “no”…  ho hum… I’ll stick to SPARK thanks… 🙂


Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK

For a long time at Praxis/Altran, we tried to publish results from projects,
particularly those using SPARK. Sometimes we succeeded, but more often than
not the projects or clients weren’t happy with the idea, so the projects
and their results remain pretty much invisible.

I wanted to write a review paper going over all the projects for a while,
and the opportunity finally arose with this year’s Interactive Theorem Proving
Conference (ITP 2014) in Vienna, where I was asked to deliver some sort of keynote.

So…we sat down and tried to write a “life and times of theorem proving
with SPARK”, starting with the SHOLIS project in 1995, and (finally!)
closing with some data from the NATS iFACTS project and some other more
recent efforts. We also decided to alternate the project stories with
the technical developments in the language and toolset, so the story
closes with a preview of SPARK 2014, which is basically a complete
reboot of the language and toolset.

In the Summer, I was in the middle of setting up Protean Code and doing
a few other things, so I couldn’t attend the conference in the end, but
Florian Schanda from SPARK team was able to go in my place, and did a great
job presenting the story.

Having actually read Springer’s copyright assignment form for the N’th
time, I realised that I could put it up here for those that don’t have
access to LNCS online.

The full reference is

“Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK”
Proc Interactive Theorem Proving 2014. July 2014. Springer-Verlag LNCS, vol 8558, pp. 17 – 26.
DOI: 10.1007/978-3-319-08970-6_2

The final publication is available at Springer via

A (short) talk about PSP…

At the recent TVS Intelligent Testing event in Bristol, I was asked to give a 20-minute talk about PSP. This seemed like a challenge, so I went for it…is it possible to say something useful in such a short time? How fast can I actually talk? Did any of the jokes work? The slides and audio track are now on-line, thanks to the folks at TVS. Click here to see what happened.