David Crocker's Verification Blog

Hi, I’m David Crocker, CTO of Escher Technologies. We make software development tools to help you write safety-critical and other high-integrity software. Our emphasis is on using automated mathematic proof to make sure that the software meets its requirements. Of course, that’s only possible if you know what the requirements are in the first place! Requirements often change through the lifetime of the software – or even while the initial version is being developed – so of course our tools also cope with changing requirements.

Up till now, we’ve mostly concentrated on tools that let you express specifications, refine them if necessary and then generate code (see http://www.eschertech.com if you want to know more). However, we’ve found that in much of the embedded world, many developers prefer to write the code by hand – and most of them are writing in C. So we’re also looking at  automatic proofs of correctness for embedded software written in C and C++. For example, do you use assertions in your C/C++ code? Wouldn’t it be great if a tool could automatically prove that those assertions are true, or else tell you why it “ain’t necessarily so” ? Tools to do that sort of analysis is what our business is about.

We’re currently using two different tools to verify C programs. One is Vcc from Microsoft Research. The other is our own, which we call ArC. That’s short for Automated Reasoning for C. It differs from Vcc in that it doesn’t handle concurrency, does handle a few features that Vcc doesn’t (e.g. floats and doubles), and is designed for a subset of C suitable for critical systems, with a few C++ features thrown in. Which one is best for you depends on what you are trying to do.

In future posts I’ll talk about how we subset C/C++ to make it both safer to write in and easier for tools to verify, and some of the problems in doing automatic verification of C/C++.