coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Verification of C++ Code

From: William Mansky <wmansky AT CS.Princeton.EDU>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Verification of C++ Code
Date: Fri, 8 Jun 2018 09:43:07 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wmansky AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=wmansky AT cs.princeton.edu; spf=None smtp.helo=postmaster AT greenlight.cs.princeton.edu
Ironport-phdr: 9a23:rylT4hTjKFvp8gi4MeWBdeIxQ9psv+yvbD5Q0YIujvd0So/mwa6yZB2N2/xhgRfzUJnB7Loc0qyK6/2mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbN/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/nzJhMx+jKxVoxyvqBJwzIHWfI6bO+Fzfr/fcN4AWWZNQshcWixHD4ihb4UPFe0BPeNAoob9plsOqR++BQi2C+Pq1zRGgWX53ash0+QiEQDNwQstHtwLsHvOqtX1L6QSUOCuwaTW0DvPdelY2S386IjObh8uv+2MXbV2ccbLxkchGQ3Kg0yWpIf4MT2V0eENvHKa7+pmTe+vk3QnqwB3ojez2Mgslo7JhoQPxl/a6Cp53YA4LsC7Rk5jedOoDYVcuiKAO4drX88uXXtktDs0x7AHo5K2fjYGxIw6yxPQd/CLaZWE7xH/WOqLPzt1hH1odKi8ihuy90Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWHReF98Vm/1jaJ0wDT6+5EIUAolabBN5Eh2aQ8loIJsUTCGC/5hFv5jLORdkUi4OSn9fnoYqj+qp+dMY97lB3+P7wzlsChAuk0KBUCU3WF9eimybHu80z0TK9Ig/EoiqXZtYrVJcUfpq63GQ9V1YMj5g6xDjejytsYm2IHLFFFeR+ck4fpIEvCIOjiDfe+hVSjjClkx+zBPr3nGJnCMGXMkKr5cbZn90Fc0BYzzcxY559MFr4BJ+vzVlbtu9zcEx82KBe5w/3nCdV4zoMRQ3iDAq6fMKPIsF+H/PgjI+eWZNxdhDGoIP88ovXqkHURmFkHfKDv04FERmq/G6FZIkGdYHPpyvIIF3wJr0JqU+njjkaBQBZ4XDCKRaM67TwnD4TgIKv+ENP+yIed1Tu2S8UFLltNDUqBRC+xJte0HswUYSfXGfdP1zkNVLyvUYgkjEH8vxS806BmKOHZ5ioe85/vyYosvrGBpVQJ7TVxSv+l/SSVVWgtzjEjfHkOxqF5qkFhzVHF/IRF0aQBSI5joshRWwJ/Dqbyiux3D9eoC1DOZNqETlKnTdW6RzoqCMorwtkFblp6HZOvgg2Rhyc=

Hi, Richard,

Currently there are no plans to extend the Verified Software Toolchain to C++, and there's enough additional semantic complexity that it's not likely to happen anytime soon. I'd be happy to talk about my experience using VST to verify C programs, though! I've used it to verify several small but reasonably complicated programs, including concurrent programs, and found it time-consuming but quite doable.

Best,

William

On 6/7/2018 2:34 PM, Richard Ford wrote:

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