That other software company has a some brilliant people working on verifying their source code. Their approach is hardcore and seems quite good. Their recipe to robust C# (applying this to C is research-in-progress, C++ isn’t yet considered) code is:
- sprinkle pre/post-conditions for functions. Reduce annotation labour by additional rule inference
- dataflow analysis to verify type-system stuff like not-null annotations
- Abstract interpretation + model checker to enforce pre/post-conditions
- BoogiePL intermediate language. Anything can be accomplished by an awesomely named intermediate language!
Resulting code runs fast has a lot fewer bugs than code without all this fancy machinery. Unfortunately, the benefits can only be reaped if a whole program gets annotated. Otherwise, the model checker gets frustrated. Essentially the language being checked is turned into another much safer (more boogie!) language. I’m looking forward to the day (that will never come) when all new C code is written this way.
If adding these to source code makes you rewrite the whole program, wouldn’t it be easier to invent another low-level language that comes with safety by default?
I am guessing that the dehydra method of checking for a relatively small number of application specific bugs is the most practical approach available and it will get us 60% towards Boogieing. Now that elsa has support for preprocessor macros it should be possible to specify non-formal pre/post-conditions to check for common errors. It’s merely a complicated question of defining what should be checked for.
That other company isn’t the only vendor working on this stuff. There brilliant people taking a somewhat different (and open source) approach.