Formal verification of MISRA-C programs

Questions and discussions about MISRA C not fitting under migration or rules forums

Moderators: misra-c, david ward

Post Reply
dcrocker
Posts: 7
Joined: Fri Oct 07, 2005 7:46 pm
Company: Escher Technologies Ltd.
Location: Ash Vale, Surrey, UK
Contact:

Formal verification of MISRA-C programs

Post by dcrocker » Mon Mar 29, 2010 12:17 pm

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
David Crocker
Escher Technologies Ltd.
http://www.eschertech.com

dcrocker
Posts: 7
Joined: Fri Oct 07, 2005 7:46 pm
Company: Escher Technologies Ltd.
Location: Ash Vale, Surrey, UK
Contact:

Re: Formal verification of MISRA-C programs

Post by dcrocker » Mon Jan 31, 2011 9:58 am

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
David Crocker
Escher Technologies Ltd.
http://www.eschertech.com

Post Reply

Return to “General Questions”