Re: [SystemSafety] systemsafety Digest, Vol 44, Issue 32

From: Roderick Chapman < >
Date: Wed, 30 Mar 2016 15:38:39 +0100


>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?


The System Safety Mailing List
systemsafety_at_xxxxxx Received on Wed Mar 30 2016 - 16:38:51 CEST

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:08 CEST