coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Andrew Appel <appel AT CS.Princeton.EDU>
To: coq-club AT inria.fr
Subject: [Coq-Club] VST release 1.7
Date: Wed, 27 Jul 2016 14:10:58 -0400 (EDT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=None smtp.helo=postmaster AT greenlight.cs.princeton.edu
Ironport-phdr: 9a23:YSM90RGkNw2k8+UuqwBONJ1GYnF86YWxBRYc798ds5kLTJ75pMiwAkXT6L1XgUPTWs2DsrQf2rKQ7f2rADVZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxib35osSKKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCKJ6mERTS0/igJFB0CR5QniU5PZmRC8jvB83iKXIcrwC50YZGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

I am pleased to announce release 1.7 of the Verified Software Toolchain.

This release includes the Verifiable C program logic, compatible with

the recently released CompCert 2.7.1 and Coq 8.5pl2.

You can obtain it here:

This release does not have many new features since Verifiable C 1.6,

but verifications do run much faster (and in less memory) thanks to

Coq 8.5's significant performance improvements compared to Coq 8.4.

-- Andrew Appel