SPARK Makes History

by Yannick Moy in Formal Verification, Events, Papers and Slides – October 29, 2014

The SPARK technology has had for a long time a passionate and very talented advocate named Rod Chapman, who relentlessly published and presented the successes in applying formal program verification with SPARK in industrial projects. Rod is no longer involved in SPARK development, but he gave a very interesting account of the history of SPARK in a paper and a presentation (see below) for a keynote at ITP conference, which completes the book chapter written by Ian O'Neill in 2012 (unfortunately Altran does not provide a free copy of this chapter on their website anymore).

One of the most interesting findings for me is how much automation and interaction have always been important along the way. Plus the paper gives the original (in both meanings of the word) acronym for SPARK...

Papers

comments powered by Disqus