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

[Peter Bishop]

I am trying of think of cases where this could actually happen.

The only things I have come up with so far are:

- cosmetic changes (white space characters and comments)

- changes to unreachable code

Any other ideas?

On 14/11/2019 16:40, Gergely Buday wrote:
> 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 <mailto: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 <mailto: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
>     <http://shape-of-code.coding-guidelines.com>
>     >> _______________________________________________
>     >> The System Safety Mailing List
>     >> systemsafety at TechFak.Uni-Bielefeld.DE
>     <mailto: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
>     <http://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

-- 

Peter Bishop
Chief Scientist
Adelard LLP
24 Waterside, 44-48 Wharf Road, London N1 7UX

Email: pgb at adelard.com
Tel:  +44-(0)20-7832 5850

Registered office: 5th Floor, Ashford Commercial Quarter, 1 Dover Place, Ashford, Kent TN23 1FB
Registered in England & Wales no. OC 304551. VAT no. 454 489808

This e-mail, and any attachments, is confidential and for the use of
the addressee only. If you are not the intended recipient, please
telephone 020 7832 5850. We do not accept legal responsibility for
this e-mail or any viruses.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191114/78e064fc/attachment-0001.html>