[SystemSafety] Fetzer
Roderick Chapman
roderick.chapman at googlemail.com
Wed Jun 19 18:35:06 CEST 2019
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
More information about the systemsafety
mailing list