coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Verification of C++ Code

From: Richard Ford <richardlford AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Verification of C++ Code
Date: Thu, 7 Jun 2018 14:34:49 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richardlford AT gmail.com; spf=Pass smtp.mailfrom=richardlford AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f51.google.com
Ironport-phdr: 9a23:HMG/mR/gGW0IJ/9uRHKM819IXTAuvvDOBiVQ1KB41+scTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/mhikEKjA37n3Yh9dqg65Huh+svQBzz5LWbYyTKfFwfrndfdQfRWdZQshRVjBOAoOmYIsVEuUKIOZWr47np1QTsBCzAhOsBOLzxT9InHD2x7A10+AvEQHBxgwvAskDsHvRrNrvNacSVfq5w7XPzTXGdv5b3yr25obPchAku/6MXLRwfNLJyUk1FgPFiEmfppL5PzOS0OQBqXaU4Pd9Ve+plmUpqBlxryCxysswjoTFnIEYx1De+Sln3Yo4Jce0RU5mbdOiDZBerTuVN5FsTcMnW2xouDg1yrkBuZOjeSgF0pUnxxrGZ/yDfYiE/gvvVOiRLDtlnn5ld7W/hxG98Uik1OLwTNW70FFPriZdk9nMsG4C1wDL58SZVvdw+l2t1DWP2gzJ9O1IPEA5mbDbJpI82rIwk4AcsUXHHi/4gkX2i6qWe10++uip9+vnYq/ppoWBOI9whAH+Nb4uldGkDOQ3NwgBRWmb+eCm2LL/+k35Ra1GjucqnanBrJDaOcMbq7alDA9Sy4Yv8gqwDzO70NsDhnQHN1JEeBefj4fzIV3OIfb4De2+g1u2ijtryerGbfXdBcDGKWGGm7P8d5587VRdwUw914Nx/ZVRX4sAK/L6QEO5mtvCAldtKQ2/w+/9BNFz0ZkScW2KC66ddqjVtAnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCO10NgEGGYO+AE5Sb6z0QHQYXtof3+3GpkEyHQjEov/VNXMQ4mshPqK2yLpRsQLNFADMUiFFDLTT6vBW/oIb3jPcMpokzhBUbb5DoF8jFehswj1z7chJe3RqHUV

I'm currently involved with some work where we want to verify the correctness of C++ code. I'm aware of the following two methods:

1. Use frama-c, which has been focused on C, but which has a recent (experimental) plug-in, frama-clang, that makes use of clang to effectively translate c++ code (actually intermediate representation) into the intermediate representation used by frama-c. frama-c use why3 in conjunction with smt provers and interactive provers (including coq) to prove verification conditions.

2. Escher Technologies' C++ verifier. I don't know much about this.

For verifying C code I am also aware of the Verified Software Toolchain effort (http://vst.cs.princeton.edu). Does anyone know whether there are any plans or work in progress to extend this to C++?

I would be glad to hear of any additional possibilities, or of experience any of you have had with these tools.

Thanks,

Richard L Ford

[Coq-Club] Verification of C++ Code, Richard Ford, 06/07/2018
- Re: [Coq-Club] Verification of C++ Code, roux cody, 06/11/2018
- <Possible follow-up(s)>
- Re: [Coq-Club] Verification of C++ Code, William Mansky, 06/08/2018