SPARK 16: A New Summary Table

by Johannes Kanig in Dev Projects, News – July 30, 2015

While SPARK 2014 is more modern than the older SPARK toolset, some features were missing in the new version. SPARK Pro 16, to be released in 2016, is going to play the catch-up game by introducing several features that long-time SPARK users have missed.

One of them is a reasonable summary of the verification. In the previous versions of SPARK, a tool called POGS would provide a summary of the proved, unproved and justified verification conditions, so that it was easy to see how much was already achieved and how much was still left to do. Until now, SPARK 2014 had no such summary.

The next version of SPARK, SPARK Pro 16, will produce after each run a summary table. This table lists the various check categories of SPARK, how many the program contains in total, and which of the various analyses in SPARK have discharged how many checks. For the SMT-solvers, the summary table shows the impact of each of them if several provers have been used. Finally, the number of unproved checks is also reported.

To see an example and a more detailed explanation, head for the corresponding section of the User's Guide.

comments powered by Disqus