References
About MISRA C
The official website of the MISRA association https://www.misra.org.uk/ has many freely available resources about MISRA C, some of which can be downloaded after registering on the MISRA Bulletin Board at https://www.misra.org.uk/forum/ (such as the examples from the MISRA C:2012 standard, which includes a one-line description of each guideline).
The following documents are freely available:
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.
The main MISRA C:2012 document can be purchased from the MISRA webstore.
PRQA is the company that first developed MISRA C, and they have been heavily involved in every version since then. Their webpage http://www.prqa.com/coding-standards/misra/ contains many resources about MISRA C: product datasheets, white papers, webinars, professional courses.
The PRQA Resources Library at http://info.prqa.com/resources-library?filter=white_paper has some freely available white papers on MISRA C and the use of static analyzers:
An introduction to MISRA C:2012 at http://info.prqa.com/MISRA C-2012-whitepaper-evaluation-lp
The Myth of Perfect MISRA Compliance at http://info.prqa.com/myth-of-perfect-MISRA Compliance-evaluation-lp, providing background information on the use and limitations of static analyzers for checking MISRA C compliance
In 2013 ISO standardized a set of 45 rules focused on security, available in the C Secure Coding Rules. A draft is freely available at http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1624.pdf
In 2018 MISRA published 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. This document is freely available from https://www.misra.org.uk/.
About SPARK
The e-learning website https://learn.adacore.com/ contains a freely available interactive course on SPARK.
The SPARK User's Guide is available at http://docs.adacore.com/spark2014-docs/html/ug/.
The SPARK Reference Manual is available at http://docs.adacore.com/spark2014-docs/html/lrm/.
A student-oriented textbook on SPARK is Building High Integrity Applications with SPARK by John McCormick and Peter Chapin, published by Cambridge University Press. It covers the latest version of the language, SPARK 2014.
A historical account of the evolution of SPARK technology and its use in industry is covered in the article Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK by Roderick Chapman and Florian Schanda, at http://proteancode.com/keynote.pdf
The website https://www.adacore.com/sparkpro is a portal for up-to-date information and resources on SPARK. AdaCore blog's site https://blog.adacore.com/ contains a number of SPARK-related posts.
The booklet AdaCore Technologies for Cyber Security shows how AdaCore's technology can be used to prevent or mitigate the most common security vulnerabilities in software. See https://www.adacore.com/books/adacore-tech-for-cyber-security/.
The booklet AdaCore Technologies for CENELEC EN 50128:2011 shows how AdaCore's technology can be used in conjunction with the CENELEC EN 50128:2011 software standard for railway control and protection systems. It describes in particular where the SPARK technology fits best and how it can be used to meet various requirements of the standard. See: https://www.adacore.com/books/cenelec-en-50128-2011/.
The booklet AdaCore Technologies for DO-178C/ED-12C similarly shows how AdaCore's technology can be used in conjunction with the DO-178C/ED-12C standard for airborne software, and describes in particular how SPARK can be used in conjunction with the Formal Methods supplement DO-333/ED-216. See https://www.adacore.com/books/do-178c-tech/.
About MISRA C and SPARK
The blog post at https://blog.adacore.com/MISRA-C-2012-vs-spark-2014-the-subset-matching-game 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 https://www.adacore.com/papers/compare-spark-MISRA-C-frama-c compares SPARK to MISRA C and to the formal verification tool Frama-C for C programs.