Verified Software Toolchain    DOWNLOADS

Verified Software Toolchain (Coq development)

Current release:
VST version 1.7 (July 2016), compatible with CompCert 2.7.1 and Coq 8.5pl2.

For advice on installing, see the first chapter of the Verifiable C manual, listed below.

Bleeding edge: VST Git repository

Previous releases:
VST version 1.6 (December 2015), compatible with CompCert 2.6 and Coq 8.4pl6.
VST version 1.5 (October 2014), compatible with CompCert 2.4 and Coq 8.4pl3 or Coq 8.4pl4.
VST version 1.4 (May 2014), compatible with CompCert 2.3
VST version 1.3 (April 2014), compatible with CompCert 2.1
Warning: CompCert 2.1's VERSION file erroneously contains "2.0" instead of "2.1", and we replicate this in vst/compcert/VERSION.
VST version 1.2 (November 2013), compatible with CompCert 2.1
Warning: CompCert 2.1's VERSION file erroneously contains "2.0" instead of "2.1", and we replicate this in vst/compcert/VERSION.
VST version 1.1 (September 2013), compatible with CompCert 2.0
VST version 1.0 (June 2013) compatible with CompCert 2.0

Documentation:

Verifiable C: Applying the Verified Software Toolchain to C programs (also included in doc/ directory of VST distribution).

Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014.
E-book; Hardback from publisher; Hardback from Amazon.com