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

Martyn Thomas martyn at thomas-associates.co.uk
Wed Feb 26 18:30:04 CET 2014


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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20140226/96b4fe81/attachment.html>


More information about the systemsafety mailing list