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

[Derek M Jones]

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