The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Hi Richard,

     As others have noted, verifying C++ is particularly nasty, to the extent that there are companies whose whole business model is writing parsers for the language, never mind understanding its semantics!

That being said, the Vellvm project (http://www.cis.upenn.edu/~stevez/vellvm/) is building tools to reason about LLVM IR, which is the intermediate target of the Clang compiler.

Probably not as mature as the VST, but worth keeping an eye on.

Best,

Cody

On Thu, Jun 7, 2018 at 2:34 PM, Richard Ford <richardlford AT gmail.com> 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