A MISRA-C Developer's Introduction to Program Proving in SPARK

MISRA-C is a coding standard focused on avoiding error-prone features of the C language. Most of the rules can be verified by static analysis, but 27 are undecidable. If a violation of an undecidable rule is not detected, then the resulting vulnerability can have serious negative security consequences. This tutorial will show how the SPARK language can achieve the same code quality and security objectives as MISRA-C and provide guarantees of program properties that go beyond what would be feasible with MISRA-C.