Book on SPARK 2014 Is Available

by Yannick Moy in Formal Verification, News – September 18, 2015

I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying! Here is my review on AdaCore's blog

The book is available both from the publisher's webpage or from Amazon.

All the examples presented in the book and the Thumper case study presented in chapter 8 are available as examples in the development version of the SPARK toolset. That gives an easy way to practice while reading the book: just open GPS, and select the spark_book or thumper example in menu Help-->SPARK-->Examples. There is also a brief description of both examples in the SPARK UG.

comments powered by Disqus