Phil Thornley has put up some SPARK tutorials at sparksure.com:
- Proof of absence of run-time error
- Proof Checker usage
Both tutorials contain several sections, with worked examples and exercises.
Also updated were a couple of the tools that help with SPARK proof:
- VC_View makes it easier to read and interpret SPARK verification conditions.
- PCHIF is an interface to the Proof Checker that makes it easier to recall and edit previously entered commands and to control the commands that are saved. (Previous versions of PCHIF were very unstable, but this is now sorted, thanks to Dmitry Kazakov and Maxim Reznik for their Gtk Router.)
The tools are currently only available as Windows executables.