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

[Steve Tockey]

Peter,
Consider Liskov Substitutability. The original code requires X and guarantees Y. The mutated code requires less than X and/or guarantees more than Y. The mutated code is semantically different but still “correct” in terms of satisfying the explicit requirements.


— steve

发自我的 iPad

On Nov 14, 2019, at 8:57 AM, Peter Bishop <pgb at adelard.com<mailto:pgb at adelard.com>> wrote:


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<mailto: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<mailto: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.

_______________________________________________
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191114/5cf8837d/attachment.html>