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

[Dewi Daniels]

Derek,

That's a very interesting paper. I didn't expect the average mutation score
to to be 100% (it's all too easy to write an assertion that's weaker than
you'd intended), but I did expect it to be higher than 93.18%.

I had no idea there was so much tool support for mutation testing. It
sounds like it could be a useful activity to carry out in conjnunction with
(or even instead of) structural coverage analysis.

The paper does state, "It is important to note that mutation scores are
much higher than traditionally seen in mutation testing research". Does
anyone know what mutation scores are achieved by typical test suites?

Yours,

Dewi Daniels | Director | Software Safety Limited

Telephone +44 7968 837742 | Email d <ddaniels at verocel.com>
ewi.daniels at software-safety.com

Software Safety Limited is a company registered in England and Wales.
Company number: 9390590. Registered office: Fairfield, 30F Bratton Road,
West Ashton, Trowbridge, United Kingdom BA14 6AZ


On Thu, 14 Nov 2019 at 15:16, Derek M Jones <derek at knosof.co.uk> wrote:

> 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/a6c09018/attachment.html>