[SystemSafety] systemsafety Digest, Vol 44, Issue 32

[Roderick Chapman]

 >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