There is nothing about C or C++ which would make programs written in these languages especially suitable for formal verification.
You could argue the one language which actually does lend itself to formal verification is the one which has been formally specified via operational semantics; namely, Standard ML.
There is one thing that helps about C and C++. In a safety-critical system, the entire runtime has to be certified. This isn't a problem for C and C++ because their runtimes are very minimal. DO-178b Level A-certified implementations of the standard libraries exist for various real-time operating systems. As long as you use them, you're golden.
However, any system that runs on top of a virtual machine is problematic because of how extensive their runtimes are. Developing an efficient and competitive DO-178b-certified JVM, for example, would be a huge undertaking, but so would modifying an existing JVM.
Further, anything garbage collected is a problem because you can't have any situations where a timing constraint is violated because of your garbage collector. The best way to prevent this would be to schedule, say, 50 milliseconds every second for garbage collection. But there's still a limit there where the GC can no longer keep up with the rate of garbage production, which could lead to your application running out of memory and failing. Proving that your application will never reach said limit would be hard either by static or dynamic analysis.
I actually once worked on a safety critical military application (though not DO-178b certified), and for a new version, we switched from C to real-time Java (RTSJ). RTSJ actually let's you avoid unpredictable GC altogether through what is called "scoped memory" in your critical threads, and provides real-time scheduling if run on a RTOS.
We switched because we wanted to reduce the risks of bugs, but you must remember that in most mission critical applications, one must consider failure not only in the software. You use redundancy - in the software, in the hardware, and in the network. We even used several separate power systems and several redundant generators.
Interesting, thanks! I didn't know about RTSJ and a cursory search in preparing my earlier comment only popped up links that looked bitrotted, so I assumed it wasn't a widespread technology.
It isn't widespread. Then again, hard real-time systems aren't widespread either. I think Boeing was (maybe still is) using RTSJ. The only downside it has is increased RAM footprint relative to C(which makes it unsuitable for very limited devices) and a small performance hit relative to regular Java because some classes need to be compiled to machine language ahead of time (the Hotspot JIT can do some very nifty optimization at runtime, but those come at a cost of non-determinism. Real-time systems always trade performance for determinism).
That's exactly the reason why C, C++ and Ada continue to be the primary choices.
There are a few interesting developments regarding Java for safety-critical and mission-critical applications. One is JSR-302, which is defining a safety-critical subset of Java which will not have garbage collection and will use of a run-time stack rather than a heap for temporary object allocation, the removal of dynamic class-loading, changes to task scheduling and a smaller standard library. These should make it possible to certify JSR-302-compatible Java runtimes and applications for safety-critical and mission-critical tasks.
The second is DO-178C, the follow-on to DO-178B, which will incorporate additional work on the certification of object-oriented languages such as Java.
I agree. It depends on what subset of C and C++ is used. If macros are used the only way to actually verify the code will be to pre-process it. Worse is if templates are used. Some templates don't even finish compiling.
Most likely no one will write such a template in a mission critical system. However, from a formal verification standpoint the only way to verify the code is to check the binaries.
You could argue the one language which actually does lend itself to formal verification is the one which has been formally specified via operational semantics; namely, Standard ML.