A Comparison of SPARK with MISRA C and Frama-C
Both SPARK and MISRA C are programming languages intended for high-assurance applications, i.e., systems where reliability is critical and safety and/or security requirements must be met. This document summarizes the two languages, compares them with respect to how they help satisfy high-assurance requirements, and compares the SPARK technology to several static analysis tools available for MISRA C with a focus on Frama-C.
Written by Johannes Kanig, AdaCore
- 2016-10-SPARK-MisraC-FramaC.pdf - (569 KB)