The Coq mailing list

[Chan Ngo <chan.ngo2203 AT gmail.com>]

Dear Andrew,

Thank you so much. Somehow I would like to look at this tool. As I understand, the correctness of the tool’s development is guaranteed by CompCert (a formal certified compiler). I have a quick question:

How do we compare this tool with other deductive verification tools for C programs (i.e., Why3, Frama-C)?

Thanks and happy new year,

Chan

On Dec 31, 2015, at 7:29 PM, Andrew Appel <appel AT CS.Princeton.EDU> wrote:

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