HOW TO CHECK THE EXAMPLES:
- You need an installation of the Why tool (tested with version 2.26)
- The Why-Coq library (distributed with the Why tool) is needed to check the Coq verification results
- The files with .mlw extension contains the product program and the relational specification. The corresponding files with extension .v are the formally verified proof obligations that are generated by the Why tool (from the files with extension .mlw).
Automatically discharging proof obligations
The Why tool implements a set of interfaces to a number of automatic theorem provers. With the exception of static_caching.mlw and interchange.mlw, all verification conditions can discharged by a combination of the Alt-Ergo, Simplify, CVC3, and Z3 provers.
The graphical interface of Why is recommended to test the examples. Running "gwhy loop_pipelining.h" opens the following window:
To check the examples with a ".c" extension, you must call the Frama-c tool with the jessie plugin, e.g.: "frama-c -jessie [filename.c]".
COQC Checking
Most of the examples, with the exception of static_caching, can be checked
by typing
coqc [filename]
(tested with Coq version 8.2pl1 )
(notice that a proper installation of the Why-Coq libraries is required)
The example static_caching must be checked with
ssrcoq [filename]
(you need the SSreflect Coq extension installed.)
For a short explanation of each of the examples please refer to the long version of the paper.