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 http://dx.doi.org/10.1007/978-3-319-08970-6_2