[SystemSafety] systemsafety Digest, Vol 63, Issue 13

[Rod Chapman]

>SPARK Pro and Frama-C are PDEs. A FM is first and foremost a method. Both
SPARK Pro and Frama-C use
>FMs, for example SPARK Pro uses Bergeretti-Carre information flow analysis
integrally.  The SPARK
>Examiner uses Hoare Logic for static analysis, as well as other methods.

Minor technical clarifications...

1. We have always SPARK is a formal _language_ owing to it having a
formally stated and
unambiguous semantics. This was always a non-negotiable design goal since
the very earliest days.
More recently, DO-333 defines "formal language" and "formal analysis" in a
manner that SPARK also
meets.

2. We would regard the use of the SPARK toolset as a "Formal Method" since
the
analyses were always designed to be sound.  See DO-333 again which,
somewhat pleasingly (thanks to Duncan and Kelly), provides a useful
definition.

3. The older SPARK83/95/2005 toolset (aka "The Examiner") does information
flow analysis using the Bergeretti/Carre scheme (ACM TOPLAS Jan 85),
and an implementation of Hoare logic for VC Generation.

4. The newer "SPARK 2014" toolset is different.  Information-flow is
done by construction and analysis of Program Dependence Graphs (PDGs)
which are far more general and mean we can analyse a far larger language
subset.  VCG in SPARK2014 is done by translation to Why3ML and
use of the Why3 VC Generator, and a number of underlying proof
engines such as CVC4, Z3 and Alt-Ergo.

 - Rod
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171026/5f657e1e/attachment.html>