AdaCore Blog

New Book About SPARK 2014

by Yannick Moy

If you're somewhat interested in formal methods applied to software, but you never had the chance to really look at it, now is the time! Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College have written a truly essential book for getting up to speed with formal verification using SPARK. I really love this book, and here are the aspects I love most:

  • It does not assume you know static analysis. It does not assume you know logic. It does not assume you know Ada. Instead, it introduces all the concepts that are useful for using SPARK where needed, with a clarity and simplicity of exposure that is remarkable.
  • It was written by very experienced users and teachers of the technology, but not by the tool builders (us at AdaCore and Altran). So they focus on the application of the technology in software engineering (in the problem domain) rather than on the technology prowesses (in the solution domain), which is a typical bias for tool builders writing on their technology.
  • It is very practical, full of examples that illustrate all the concepts they explain and the tips they give on the actual practice of an engineer applying formal verification with SPARK on her code.

I see this book as a glorified User's Guide to SPARK, and I recommend it to anybody who either wants to have a first look at SPARK, or actually starts using it for real. In fact, we also try to apply the principles above in the SPARK User's Guide, but their book is definitely a better entry door to the technology, while the User's Guide tries to be its map. Besides the publisher's webpage, you can find it on Amazon and many other online bookstores.

For those in academia who would like to teach SPARK, the book is ideally structured with a summary and exercises closing each chapter. All examples are available from the publisher's webpage (see Resources and Source code) and the final case study on a time stamp server is available from one of the authors's github. You may also get a free copy of the book from Cambridge University Press to evaluate it for your course (see the publisher's webpage).

Posted in #SPARK    #Formal Methods    #Teaching   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK 2014, a product he presents in articles, conferences, classes and blogs (in particular www.spark-2014.org). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.