Literatura

J. Barnes. SPARK: The Proven Approach to High Integrity Software. Altran Praxis, 2012. (dotyczy starszej wersji)
J. McCormick, P. Chapin. Building High Integrity Applications with SPARK. Cambridge University Press, 2015.
SPARK 2014 Toolset User's Guide. AdaCore and Altran UK Ltd
SPARK 2014 Reference Manual. AdaCore and Altran UK Ltd

Mordechai Ben-Ari. Principles of the Spin Model Checker. Springer, 2008.
Gerard J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.

Deductive Program Verification with Why3. A Tutorial. Lecture in the Logic Semantics group at IoC.