SPARK Ada for the MISRA C DeveloperΒΆ

This book presents the SPARK technology β€” the SPARK subset of Ada and its supporting static analysis tools β€” through an example-driven comparison with the rules in the widely known MISRA C subset of the C language.

This document was prepared by Yannick Moy, with contributions and review from Ben Brosgol.