Spark Pro – High Assurance by Design
High Assurance by Design
SPARK Pro BlackBelt Edition adds support for three optional components of the toolsuite: the Proof Checker, the RavenSPARK language option, and the SPARKBridge technology (preview).
SPARK Proof Checker
The Proof Checker is an interactive proof tool that uses the same logic and inference engine as the Simplifier. It can be used to complete the proof of any VCs left undischarged by the Simplifier, if the assurance requirements of the project are high enough to warrant a fully formal proof. Support for the Proof Checker is only available with the SPARK Pro BlackBelt Edition.
RavenSPARK Language Option
The RavenSPARK option brings the power of Ada’s Ravenscar tasking profile to SPARK, enabling engineers to design concurrent software without sacrificing verification or assurance. RavenSPARK is specifically design to be compatible with hard real-time operating systems, all implementations of the Ravenscar profile, and to be amenable to the static analysis of worst-case execution time, schedulability and memory consumption. Support for RavenSPARK is only available with the SPARK Pro BlackBelt Edition.
SPARKBridge technology (preview)
SPARKBridge, a ViCToR-based technology bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers such as Alt-Ergo, allows the use of alternate provers for automatically proving Verification Conditions.
The SPARK programming language is not sponsored by or affiliated with SPARC International Inc and is not based on the SPARC(tm) architecture.