David Crocker's Verification Blog

Hi, I’m David Crocker, founder of Escher Technologies. I’ve been working in software development for many years. Most of my experience has been with C, C++ and Perfect, and I’m also competent in several other languages, particularly C# and F#.

I’ve more than 20 years of experience of using C and C++ to write high-reliability software, and I contributed to the MISRA C 2004 and MISRA C++ standards. Although C and C++ are far from ideal, they are well-supported by compilers and tools, and their weaknesses and vulnerabilities are well-understood. That makes them reasonable languages to subset for safety-critical work. In the case of C++, the sheer size of the language makes it difficult to define a safe subset that is guaranteed to exclude all the questionable areas. So, instead of listing the features you are not allowed to use, I think it better to define subsets that say which features you are allowed to use – in addition to the features of a C subset such as MISRA-C. That’s one of the themes of my blog. There’s probably a need for more than one subset, suited to different integrity levels.

One of the problems with developing critical software is that it is impossible to test thoroughly. There are some very good testing tools on the market, but unless your software is very simple, it’s just not possible to cover all possible inputs in a reasonable amount of time. So for really critical systems, you need formal verification too. As a minimum, formal verification can show that your program will not suffer from any run-time nasties such as writing past the end of an array, dereferencing a null pointer, or dividing by zero. You can also use formal verification to prove that your program satisfies certain properties, such as safety properties.

There are two ways of producing formally verified software. One is to start from a formal description of the required behaviour, and generate code from that description – perhaps with some intermediate human-assisted refinement. That’s what our product Perfect Developer is designed to do. Or you can write a program in a verifiable subset of a standard programming language, annotate the program with specifications, and use a tool to prove that the specifications are met and there will be no run-time errors. That’s the goal of our C/C++ verification project, and it’s what the Examiner does for SPARK Ada. Or you can do some of both: express the specification and design in a formal model, verify it at that level, then hand-code the design in C/C++ or SPARK Ada and verify it again. For example, Perfect Developer and SPARK Ada are used together to develop critical airborne software in the defence industry.

Formal verification used to be expensive, because theorem proving had to be done by hand, or on a computer with human assistance. We pioneered the use of fully automatic theorem proving in Perfect Developer, and we’re now using the same technology on C/C++. We can’t promise to prove every true theorem – a perfect theorem prover cannot exist – but we do achieve successful proof rates of 95% to 100%, depending on the complexity of the software.

If you want to get in touch, you can compose my email address by prepending my initial to my surname and using the eschertech.com domain. Or go to http://www.eschertech.com and fill out the contact form.