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

[Gergely Buday]

This means that Coq verification scripts are 7% robust against slight
changes in definitions. That's important in verification, ask any developer
who maintains large scale verification projects.

Derek M Jones <derek at knosof.co.uk> ezt írta (időpont: 2019. nov. 14., Csü
16:35):

> All,
>
> Some interesting results from the mutation analysis of Coq proofs:
> http://cozy.ece.utexas.edu/mcoq/
>
> Mutation analysis introduces a mistake into code, by mutating existing
> code at some point (there is a small cottage industry working on new
> mutation operators), and the modified code is executed in some way.
>
> A common research use (not much used in industry) is using mutated
> code to check the quality of a test suite, i.e., a thorough test
> suite will detect the added mistake.
>
> "Mutation Analysis for Coq" does what it says on the tin.  It mutates
> Coq proofs, and then checks whether the verification fails (which it
> should do).
>
> In 7% of cases (6.82% to be exact), verification succeeded (averaged
> over all mutations).
>
> So, those of you who have paid for Coq proofs to be written for your
> software.  If the proof contains a mistake, there is something like
> a 7% chance it has gone undetected.
>
> 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?
>
> --
> Derek M. Jones           Software analysis
> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription:
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191114/5d7742ee/attachment.html>