Prototyping Static Analysis Certification using Why3
Tools and experiments
Source code
- Download the Why3 development [zip].
- The archive contains:
- the theories describing the language and implementing
auxiliary functions used in the semantics: semantics_array.why;
- the interpreter and the axiomatisation theorems: interpreter_array.mlw;
- the theory implementing the Factorial program and the
result of the interval analysis: pgm_factorial.why;
- the theory implementing the Binary search program and
the result of the polyhedral analysis: pgm_binarysearch.why;
- as a bonus, the theory implementing the Factorial program and the
result of the polyhedral
analysis: pgm_factorial_polyhedra.why;
- an axiomatisation of non-polymorphic maps necessary for
the definition of stores: mmap.why;
- folders containing the historic of proofs realised in
why3ide for each file.
- To test the approach, one can either use the why3ide tool
to reproduce the proofs done in the article or use the why3ml
tool on the interpreter file and the why3 tool on the file
containing only theories (that is, all files with
the .why extension).
In both case, you can launch the executable in a terminal as
long as the working directory contain all the files of the Why3
development. Either,
- for the IDE : $ why3ide -I . file_I_want_to_check.why &
- or, for using the command line executables with a particular
prover:
- for Why3 theories: $ why3 -I . -a prover_to_launch file_I_want_to_check.why
- for Why3 modules (the interpreter in our case): $ why3ml -I . -a prover_to_launch file_I_want_to_check.mlw
The proof of binary search is even
simpler than the one described in the article, as a few
syntactic modification tested since the submission lead to
better performance of the Z3 ATP. Most theorems are now
discharged directly, and only one needs transformations and
collaboration with Alt-Ergo.
Tools