On 12/12/2014 11:00, systemsafety-request at lists.techfak.uni-bielefeld.de wrote: > The new Mission Computer software was still in > Ada, but not in a SPARK compatible subset That's interesting. Who paid the bill for you to put it right and repeat the analysis? Lockheed? MoD? RAF? - Rod