Paper
F. Besson, D. Cachera, T. Jensen and D. Pichardie, Certified Static Analysis by Abstract Interpretation, Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009, Tutorial Lectures, LNCS vol. 5705. [.pdf]
Slides
| Title | [.pdf] |
| Motivations | [.pdf] |
| A certified non-interference verifier | [.pdf] |
| A certified data race analysis | [.pdf] |
| A certified lightweight array bound checker | [.pdf] |
| Tutorial: building a certified static analysis | [.pdf] |
Download
Download the Coq sources of the tutorial here (tested with Coq 8.2 and Ocaml 3.10.2).
Install:
tar xzf certified_analysis_fosad09.tgz;
cd certified_analysis_fosad09.tgz;
make
It should generate the extracted code coq.ml and two executables from it
sign and interval. Run them and enjoy !