Spark Pro – High Assurance by Design
SPARK Pro provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Praxis with the GNAT Programming Studio (GPS) development environment from AdaCore.
The SPARK Pro Subscription Package
Adacore Praxis Partnership
Altran Praxis and AdaCore have formed a long-term partnership with the intent of taking the SPARK language and toolset to a new level in technical capability, marketing and sales.
The SPARK Pro Package
SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. SPARK Pro prevents, detects and eliminates defects early in the life-cycle as the source code is developed.
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.
Frontline support is provided through GNAT Tracker, AdaCore’s web based support system.
SPARK Pro is compatible with all implementations of Ada83, Ada95 and Ada2005. A subscription to GNAT Pro is not required.
SPARK and the Tokeneer Project
SPARK was chosen as the implementation language for the Tokeneer ID Station, developed by Praxis for the NSA. A tutorial introduction to SPARK, using Tokeneer as an example, has now also been released and is known as ‘Tokeneer Discovery’. For more information about Tokeneer and Discovery follow the link below.
The SPARK programming language is not sponsored by or affiliated with SPARC International Inc and is not based on the SPARC(tm) architecture.