The official website of the MISRA association has many freely available resources about MISRA-C, some of which can be downloaded after registering on the MISRA Bulletin Board at (like the set of examples from MISRA-C:2012 document which includes the one-line description of all guidelines).

The following documents are available freely:

  • MISRA Compliance 2016: Achieving compliance with MISRA coding guidelines, 2016, which explains the rationale and process for compliance, including a thorough discussions of acceptable deviations
  • MISRA C:2012 - Amendment 1: Additional security guidelines for MISRA C:2012, 2016, which contains 14 additional guidelines focusing on security. This is a minor addition to MISRA-C, that we did not feel we needed to discuss further in this book.

The main MISRA-C:2012 document is available at a small cost from the MISRA webstore.

PRQA is the company at the origin of the first version of MISRA-C, and they have been very involved in every version since then. Their webpage contains many resources about MISRA-C: product datasheets, white papers, webinars, trainings.

PRQA Resources Library at has interesting feely available white papers on MISRA-C and the use of static analyzers:

ISO standardized in 2013 a set of 45 rules focused on security, available in the C Secure Coding Rules document. A draft is freely available at

MISRA association published in 2018 a document MISRA C:2012 - Addendum 2: Coverage of MISRA C:2012 against ISO/IEC TS 17961:2013 "C Secure" mapping ISO rules to MISRA-C:2012 guidelines, available freely from


The e-learning website contains a freely available interactive course on SPARK.

The SPARK User's Guide is available at

The SPARK Reference Manual is available at

A student-oriented textbook on SPARK is Building High Integrity Applications with SPARK by McCormick and Chapin, published by Cambridge University Press. It is sold online by Amazon and many others.

For a historical account of the evolution of SPARK technology and its use in industry, see the article Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK by Chapman and Schanda, at

The website is a portal for up-to-date information and resources on SPARK. AdaCore blog at frequently hosts posts on the latest evolutions of SPARK.

The document AdaCore Technologies for Cyber Security presents the usage of AdaCore's technology to prevent or mitigate the most common security vulnerabilities in software. See:

The document AdaCore Technologies for CENELEC EN 50128:2011 presents the usage of AdaCore's technology in conjunction with the CENELEC EN 50128:2011 standard. It describes in particular where the SPARK technology fits best and how it can best be used to meet various requirements of the standard. See:

The document AdaCore Technologies for DO-178C/ED-12C similarly presents the usage of AdaCore's technology in conjunction with the DO-178C/ED-12C standard, and describes in particular the use of SPARK in relation with the Formal Methods supplement DO-333/ED-216. See:


The blog post at reviews the 27 undecidable rules in MISRA-C:2012 and describes how SPARK addresses them.

The white paper A Comparison of SPARK with MISRA C and Frama-C at compares SPARK to MISRA-C and to the formal verification tool Frama-C for C programs.