Formal verification of MISRA-C programs

[dcrocker]

We're working on a tool to perform formal verification of programs written in MISRA-C 2004. The idea is to annotate MISRA C functions (e.g. by writing preconditions) so that we can prove automatically that array indices are always in bounds, null pointers are never deferenced, division is never by zero, and so on. Then we prove that the callers of those functions meet the preconditions... and so on up to the main program. So we aim to prove compliance with the "hard" MISRA rules like 1.2, 17.1, 17.6 and of course 21.1. We'll also be able to prove other things, such as safety properties that can be expressed functionally.

I'm interested to know the extent to which MISRA-C users are prepared to write extra annotations to get this increased level of assurance. Please reply if you have a view on this, if possible saying what safety standard (if any) you are working to.

I've also started a blog about this approach, which you can find at http://blog.eschertech.com.

Regards - David

[dcrocker]

Please note that my blog on formal verification of MISRA-C and similar code has moved to http://critical.eschertech.com. The old address (blog.eschertech.com) will be withdrawn a couple of months from now.

Regards - David