New SPARK Book
SPARK: THE PROVEN APPROACH TO HIGH INTEGRITY SOFTWARE
The new 2012 edition of John Barnes' SPARK book is now available...
SPARK is a programming language and static verification technology designed specifically for the development of high integrity software. First designed over 20 years ago, SPARK has established a track record of use in embedded and critical systems across a diverse range of industrial domains where safety and security are paramount.
This third edition of the SPARK book is a major update which covers more recent additions to the SPARK language and tools, including significant improvements to the power of the SPARK proof system and the use of RavenSPARK for multitasking programs.
From basic principles through to the use of advanced proof techniques, John Barnes provides both an informal introduction and a reference guide for those wishing to develop high integrity software using SPARK.
The following downloads are available to accompany the book:
GPL edition of the SPARK tools (Make sure you select the 2012 version of the tools on the download page.)
Source code of examples that appear in the book : Windows version
Source code of examples that appear in the book : Linux/Mac version
GPL edition of the GNAT compiler and accompanying IDE
For more information on obtaining the SPARK toolset for commercial use please visit the SPARK Pro site.
"This is the indispensable handbook for SPARK. John Barnes imparts knowledge and wisdom with wit and style."
"The key to the use of any Formal Method, is the definition of a formal notation and the creation of useful analysis tools which are sound. This book gives an excellent explanation of both of these aspects and is an invaluable aid to anyone attempting to use SPARK with the DO-178C Formal Methods supplement or without it."
"From principles of modular program design, to writing specifications, to using the SPARK tool chain to discharge proof obligations, this book gives insight and expert guidance into the process of verifying programs to be free from run-time errors."