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

[Gergely Buday]

The change was in the code, not in the specification. Changes in the code
can result in specification-conforming code.

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

> Gergely,
>
> > This means that Coq verification scripts are 7% robust against slight
> > changes in definitions. That's important in verification, ask any
> developer
>
> Mutations are random changes, which may or may not be slight.
>
> You appear to be suggesting that failure to detect 7% of random changes
> is a desirable property.  I find this surprising.  Do you think the 7%
> figure is about right (for this 'desirable' property), or should it be
> higher/lower?
>
> > 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
> >>
> >
>
> --
> Derek M. Jones           Software analysis
> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191114/c03fb0c1/attachment.html>