[SystemSafety] systemsafety Digest, Vol 66, Issue 6

[Roderick Chapman]

On 05/01/2018 11:00, systemsafety-request at lists.techfak.uni-bielefeld.de 
wrote:

> Does "100% OK" mean that 2 faults per thousand lines of code
> are OK?

No.. obviously not. It means that the prover has proved 100% of the VCs that
result from the properties you're trying to prove.

The 2 defect per kloc number comes from reading the abstract of the paper
that you cite. The full paper contains a more detailed breakdown of each
defect and whether it was in the SPARK code, or the supporting Ada. I am 
happy
to post a summary here if anyone is really interested...
  - Rod