[SystemSafety] systemsafety Digest, Vol 44, Issue 32

[GRAZEBROOK, Alvery N]

Hi Rod,

According to "Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK"
http://proteancode.com/keynote.pdf
you (or your co-author Florian) have already done something similar. In section 2.6:
** The results are dramatic. On a modern (2013-era) quad-core machine, the
** entire SHOLIS software can be re-proven from scratch in about 11 minutes, with
** only 440 undischarged VCs (compare with weeks and 2200 undischarged VCs in
** the original project).

What this doesn't do is address the *real* time-consuming part, which is to assess how much more "software functionality" is produced with a given quantity of personal effort, or whether there is some improvement in quality standard achieved. (Using whatever means you can agree to measure an amount of "software functionality").

Cheers,
	Alvery

-----Original Message-----
From: systemsafety [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of Roderick Chapman
Sent: 30 March 2016 3:39 PM
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] systemsafety Digest, Vol 44, Issue 32

 >One should also take into account that SHOLIS is a project executed a decade and a half ago,  >and the effective use of formal techniques has progressed since then, witness the information  >on IFACTS contained in the 2014 Chapman-Schanda survey paper.

Actually - more like 20 years.  I started work on coding and proving SHOLIS in late 1995.

It would be entertaining to compare the proof data (both time and completeness of the proof tools) on the hardware of the day (a single core Sun SPARCStation 20 that was shared by the whole company if I recall correctly) and tools (SPARK Toolset about version
2.0-ish) with hardware
and tools that we have today.

I recall waiting overnight or whole weekends for the prover to run on some of the bigger subprograms back in '96. Re-proof of the whole thing takes a few minutes now.

We could even re-code SHOLIS in SPARK 2014 to see how the current crop of SMT solvers (notably CVC4 and Z3) and Alt-Ergo perform in comparison to the "classic"
PROLOG-based SPARK proof tools.

Derek - would that kind of data satisfy you?

  - Rod

_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE

This mail has originated outside your organization, either from an external partner or the Global Internet.
Keep this in mind if you answer this message.



This email and its attachments may contain confidential and/or privileged information.  If you have received them in error you must not use, copy or disclose their content to any person.  Please notify the sender immediately and then delete this email from your system.  This e-mail has been scanned for viruses, but it is the responsibility of the recipient to conduct their own security measures. Airbus Operations Limited is not liable for any loss or damage arising from the receipt or use of this e-mail. 

Airbus Operations Limited, a company registered in England and Wales, registration number, 3468788.  Registered office:  Pegasus House, Aerospace Avenue, Filton, Bristol, BS34 7PA, UK.