LASER 2011 Summerschool
Elba Island, Italy
Software demonstrated during this course
Coq version 8.3 Web site
- External Coq libraries:
- External tools:
Frama-C : analysis of C programs (Web site).
- Why : program deductive analysis Web site, new generation Why3 (Web site).
- Gappa : tool to analyse floating point computation Web site
with an associated Coq library
- Alt-ergo an SMT prover for program verification
This document was translated from LATEX by