[SystemSafety] Bursting the formal methods bubble

[Derek M Jones]

Martyn,

> The NSA concluded that Z/SPARK CorrectbyConstruction beat every other
> software development approach they had experienced. Search for Tokeneer
> on line.

My searches only located congratulatory statements by the usual
suspects.

Is their an internal report that you know about (it was your company
that did the work, after all)?

Those involved seem to make a big thing about only two bugs being found.
One possible reason for such a small number of bugs is that very few
people used the software in anger.

This work found new 20 problems, of which half could lead to
system failure:
www.open-do.org/wp-content/uploads/2010/04/ERTS2010_final.pdf


-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com