Re: [SystemSafety] Scalability of Formal Methods [was: Logic]

From: Martyn Thomas < >
Date: Wed, 26 Feb 2014 17:30:04 +0000


On 26/02/2014 14:13, David MENTRE wrote:
>> I'd want to know how many proof obligations were left undischarged.
>
> Zero (0). Of course, a significant part (3.3% to 8.1% of proof
> obligations, i.e. 1,400 to 2,200) is done manually (i.e. interactive
> proofs) by a team of skilled engineers (internal or using subcontracts
> to companies specialized in such proofs).

The proof obligations from SPARK are free-standing, in that proving them requires no knowledge of the project, the application or the software, and they contain no proprietary information. Proving them can therefore be easily subcontracted. I expect that the same is true for Atelier B.

Martyn



The System Safety Mailing List
systemsafety_at_xxxxxx Received on Wed Feb 26 2014 - 18:30:16 CET

This archive was generated by hypermail 2.3.0 : Sat Feb 23 2019 - 01:17:06 CET