Verification of C Programs Using Automated Reasoning

Much of the embedded software development market has necessarily tight constraints on program size and processor power, hence developers use handwritten C rather than autocode. They rely primarily on testing to find errors in their code. We have an established software development tool known commercially as Perfect Developer, which uses a powerful automatic theorem prover and inference engine to reason about requirements and specifications. We have found that automated reasoning can be used to discharge a very high proportion of verification conditions arising from the specification and refinement of software components described in our formal specification language, Perfect. The Perfect Developer tool set can also generate code in a C++ subset or in Java, and the output code is then virtually certain to meet the stated specification, reducing the need for exhaustive testing. However, this is not helpful to developers of embedded software who are constrained to write code by hand. We therefore decided to investigate whether automated reasoning could provide a similar degree of success in the verification of annotated C code. We present our preliminary findings.