As part of the HI-Lite project, major enhancements have been made to the SPARK language and toolset. The new SPARK 2014 language is both richer and more flexible, and exploits the Ada 2012 contract-based programming features.
This will enable greater verification automation and also simplify the development of SPARK 2014 applications. The new toolset that will rely on SPARK 2014 will also provide innovative ways of combining formal verification with testing and will allow SPARK 2014 to be used incrementally in legacy projects. The first commercial release is expected in Q1 2014. For more information please visit www.spark-2014.org/
Created on Jun 18th, 2013. Updated on Jun 18th, 2013.