spark2014

SPARK 16 will contain a better way to see a summary of the verification results. This blog post introduces the new feature.

SPARK 16 will contain a better way to see a summary of the verification results. This blog post introduces the new feature.

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

The international team developing the SPARK product, usually dispersed across continents and islands (if UK still counts as an Island despite the Channel Tunnel), has gathered the last week of June to discuss the progress towards SPARK Pro 16.0, and beyond that. Here are the main points that we discussed.

The international team developing the SPARK product, usually dispersed across continents and islands (if UK still counts as an Island despite the Channel Tunnel), has gathered the last week of June to discuss the progress towards SPARK Pro 16.0, and beyond that. Here are the main points that we discussed.

It is with great sadness that I have to announce the death of Robert Dewar. Robert was President of AdaCore, and he has had a tremendous influence on the development of SPARK.

It is with great sadness that I have to announce the death of Robert Dewar. Robert was President of AdaCore, and he has had a tremendous influence on the development of SPARK.

Constants whose initial expressions depend on global variables or formal parameters can now appear in flow-related contracts. This allows more accurate specification and verification of information flow properties.

Constants whose initial expressions depend on global variables or formal parameters can now appear in flow-related contracts. This allows more accurate specification and verification of information flow properties.