High Assurance Software Development
SPARK Pro combines the power of the SPARK language and toolsuite from Altran with the GPS development environment from AdaCore in a single package. The SPARK Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.
The SPARK Language takes a radical step away from contemporary programming language design. The primary design goal is the provision of a sound verification framework and toolsuite which renders many common defects simply impossible or at least sure to be detected. The SPARK language embodies a strictly defined and enforced subset of Ada complemented by an expressive system of contracts that precisely convey the design or the specification of the program itself.
This Integrated Development Environment serves as your portal to the SPARK Pro toolchain. It provides customizable settings, browsing, syntax-directed editing, easy integration with third party tools such as Version Control Systems, source navigation, dependency graphs, and more. Learn More »
SPARK Supporting Tools
SPARK Pro also includes other supporting tools for SPARK such as a pretty-printer for contracts (SPARKFormat), a proof status summarizer (POGS), and the SPARKMake tool for generating the Examiner’s index- and meta-files.
The Examiner provides the main static analysis engine of SPARK Pro. It enforces the SPARK subset and static semantics, checks contracts for consistency with source code, and implements the SPARK information-flow analysis and verification condition generator.
The Simplifier is an automated theorem prover that processes the verification conditions (VCs) produced by the Examiner. The proof of these VCs confirms critical program properties, such as the freedom from run-time errors and exceptions, or specific safety and security properties. For well-written code, the Simplifier typically proves over 95% of these VCs completely automatically – or, in other words, less than a 5% false-alarm rate.
GNAT Semantic Analyzer
The GNAT Semantic Analyzer provides a full Ada front-end capability in support of SPARK Pro. This offers full Ada static semantic checking, style checking, and generation of cross-reference information for use within the GPS IDE. Additionally, the GNAT Semantic Analyzer can check a subset of the SPARK rules when the SPARK restriction is used.
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.
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 VCs.
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 designed 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.