David Crocker's Verification Blog

We’re now nearing the beta release of our C verification product. We’ve decided to call the product Escher C Verifier, or eCv for short. While we liked the name ArC (Automated Reasoning about C), there are just too many pieces of software already out there with ARC in the name.

The market that we’re trying to address with eCv is critical embedded systems – especially SIL3 and higher – with code written to the MISRA-C 2004 standard or similar. Restricting ourselves to a C subset in this way allows us to reduce the amount of non-trivial annotation required, aiding developer productivity. If you want to verify programs that don’t fall into the subset we handle, then there are alternatives such as Microsoft Research’s Vcc – but don’t be surprised if the annotation needed is more complex.

We’ll be presenting a case study on applying eCv to critical software at the Safety Critical Systems Club meeting on 15 September in Manchester; and we’ll be discussing the relevance of eCv to ensuring compliance with “hard” MISRA C rules at the MISRA-C meeting on 25 November in London. You can find details of these events at the SCSC website. If you’ve been following my blog and you’ll be attending one of these meetings, please introduce yourself to me in one of the breaks.

Information about eCv itself is available at the Escher Technologies site.