[SystemSafety] Fetzer

[Roderick Chapman]

On 19/06/2019 16:36, Derek M Jones wrote:
> Proponents of particular languages invariably claim 'magical'
> properties for the language.  No evidence is ever provided, and
> apart from a handful of exceptions, no experimental evidence
> exists.  It's all personal opinion. 

Here are some SPARK project and published references:

SHOLIS (IEEE Transaction on SE, August 2000)

MULTOS CA (IEEE Software, Jan/Feb 2002)

C130J (Andy German's paper in CrossTalk, and Jim Sutton's "Lean Software 
Strategies" book)

Tokeneer (various articles, but the project summary report is the best 
place to start)

NATS iFACTS (summary data in the article below...)

Oh.. and see "Are we there yet? 20 years of industrial theorem proving 
with SPARK" from the ITP 2014 conference, which contains a summary of 
the data from those and a few other projects. Available here: 
https://proteancode.com/wp-content/uploads/2015/05/keynote.pdf

Now watch as Derek dismisses all this as soap-powder marketing... :-)

  - Rod