Formal methods in C++ for safety critical software

Question

Looking at C, C has good support for formal methods that can be used in-code(frama-c, VCC, verifast). C++ doesn't seem to have any comparable as far as I can tell.

What formal methods are available for reasoning about safety-critical software written in C++?

Answer 1

A medical company I work with uses Coverity and Klocwork to check the code for possible problems such as resource leaks and uninitialized pointer getting used.

However, these are tools and not standard for safety critical code.

What I have seen is that MISRA has been working on a standard for C++. They started with C way back, and start work on C++ about 5 years ago or so. One big problem is that the MISRA standard for C++, for example, says you should not use templates. That really limits what you can do in C++. However, you could use that document as a starting point. You may want to limit templates used in your software to what comes in the standard library and boost, for example.

Note that Klocwork has an extension for MISRA C++.

Yet, one of the best way to write good code is to test it with unit tests and integration tests. I have found with years that this is way more reliable that most other methods.