The Coq mailing list

[Andrew Appel <appel AT CS.Princeton.EDU>]

I am pleased to announce the release of version 1.6

of the Verified Software Toolchain, compatible with CompCert 2.6.

It includes the Verifiable C program logic, a higher-order separation logic

for reasoning in Coq about the correctness of C programs.

http://vst.cs.princeton.edu/download/

This release of Verifiable C has substantial improvements in robustness,

efficiency, usability, and documentation.  (All recent versions are proved

sound in Coq w.r.t. the CompCert operational semantics; "robustness"

refers to the capabilities of VeriC's proof automation system in assisting

users in building C-program correctness proofs in Coq).  

Qinxiang Cao, Lennart Beringer, Josiah Dodds, Jean-Marie Madiot, Santiago Cuellar,

and Gordon Stewart contributed to the development of this version.

Recent proofs in Verifiable C include:
correctness of OpenSSL SHA-256,   http://www.cs.princeton.edu/~appel/papers/verif-sha.pdf

correctness of OpenSSL HMAC,  http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf

correctness of mbedTLS DRBG; specification of mbedTLS AES-256.

(There are plenty of applications other than crypto primitives, but crypto is a

convenient source of small, well-specified programs whose correctness

is actually important to people. :-)

Andrew W. Appel

Princeton University