From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,b03962e55f213a92
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news2.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nntp.club.cc.cmu.edu!feeder.erje.net!eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: What is SPARK about?
Date: Sun, 13 Jun 2010 09:11:54 +0100
Organization: A noiseless patient Spider
Message-ID: <m2k4q3xsfp.fsf@pushface.org>
References: 
 <d41d71f3-907b-4948-b2b8-784a12439d4c@g39g2000pri.googlegroups.com>
	<db42cb26-7ab8-4484-be97-74ad605c04ac@5g2000yqz.googlegroups.com>
	<b9700a96-84d1-4c4b-8e3a-70ae62e2cda7@a39g2000prb.googlegroups.com>
	<hv1qq6$g1u$1@news.eternal-september.org>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 13 Jun 2010 08:11:56 +0000 (UTC)
Injection-Info: mx03.eternal-september.org;
 posting-host="KCXegvZb5vh43D+f3BR6Ew";
	logging-data="13164"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18vYWUH0W7xw0U+so4VLIx8qJigs/EMRUs="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (darwin)
Cancel-Lock: sha1:3WyDw7e3d249UzU0E5preLhsSTY=
	sha1:Q5niH2O5eNwFPv8VfYYfc8wXXKI=
Xref: g2news2.google.com comp.lang.ada:12643
Date: 2010-06-13T09:11:54+01:00
List-Id: <comp.lang.ada>

"J-P. Rosen" <rosen@adalog.fr> writes:

> Claude a écrit :
>> Feb 2010, the ERCIM Working Group on Formal Methods for Industrial
>> Critical Systems stated:  “There is a lack of precedents where formal
>> methods have been proven to be effective.”
>> http://www.inrialpes.fr/vasy/fmics/
>> 
>> Did the ECRIM overlook iFACTS?
>> 
> More surprisingly, did they overlook Meteor (100% automated line 14 of
> the Parisian subway, in B+Ada) ?

This is very relevant -- took a little googling (meteor paris metro ada
formal b):
http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf