[SystemSafety] 7% of mistakes in Coq proofs go undetected

[Martyn Thomas]

I can't speak for Coq, but I know that universities have experimented
with the NSA security system that Rod Chapman put on line as a complete
worked example of a SPARK development. I think Rod has written up the
experiences - it will be in the archives of the safety list.

Praxis offered a free 10 year guarantee of free fixes within tight time
constraints. On CDIS, I think we had one or two claims that we had to
investigate, but mainly NATS called to ask for a re-run of the training
course on how to boot the system, because the operators hadn't had to do
it for so long they might have forgotten how.  I think Altran may still
offer something similar. Of course, if the customer were to alter the
software it would break the guarantee.

I think customers should ask their suppliers why their customers should
trust the system to support their business if the supplier doesn't trust
it enough to offer a guarantee.

Martyn

On 14/11/2019 15:16, Derek M Jones wrote:
> Do companies offering "proofs of correctness" provide fix-it for free
> guarantees?  Or do the claims of correctness never make it from the
> marketing department to a signed contract?

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191114/1cd0cde6/attachment.sig>