SPARK Pro

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 Altran Praxis with the GNAT Programming Studio (GPS) development environment from AdaCore. SPARK Pro has an enviable track-record in many industry sectors, such as aerospace, rail, nuclear and security, and has been used to meet or exceed all known industry guidance and standards at the highest assurance levels.

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.

Language and Toolsuite

SPARK Pro combines the renowned SPARK language and toolset from Praxis with the GPS IDE and GNAT Tracker support system from AdaCore. The toolsuite comprises the SPARK Examiner, Simplifier, Proof Checker, and other supporting tools. Learn More »

Black Belt Edition

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). Learn More »

The Choice For High Assurance Programming

SPARK is unique – it’s the only modern imperative programming language designed with the provision of sound static verification as the primary design goal. Through simplification of the language and the addition of contracts, SPARK also offers verification which is fast, deep, constructive and exhibits a remarkably low false-alarm rate. No other programming language or verification tools can offer this combination.

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.

Read the press release »

The Tokeneer Project: A hands on look at an NSA Funded, highly secure biometric software system.

Knowledge Center

Webinars

Introducing SPARK 10.1

February 21, 2012
The InSight webinar series continues with a presentation on the new features of the AdaCore/Altran Praxis joint offering – SPARK Pro 10.1. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

SPARK 10.1 includes the following enhancements:
- Generics Phase 1 - Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
- Dynamic Flow Analyser and VCG Heaps
- Unicode characters now allowed in strings
- Improved use of types and subtypes in FDL
- Improvements to Simplifier tactics and performance
- Auto-generation of refinement rules
- Improvements to SPARKBridge
- New SPARKClean utility
This webinar will include a demo and Q&A session with the developers of the SPARK Pro toolset.
Introducing SPARK 10

July 05, 2011

The InSight webinar series continues with a presentation by Robin Messer on the new features of the AdaCore/Altran Praxis joint offering – SPARK Pro 10. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

SPARK Pro 10 is a major release including many new features – automatic selection of flow analysis mode, language profile for SCADE KCG, support for explicitly derived numeric types, addition of the SPARKBridge preview for Windows, library additions, and improvements to the SPARK proof tools.

Developer Gems

Gem #80: Speedy Shift and Rotate in SPARK

Ada Gem #80 — This Gem covers a topic that I recently encountered while working on a crypto algorithm in SPARK: how to use Ada's predefined shift and rotate functions with modular types from a SPARK program.
Gem #76: Tokeneer Discovery - Lesson 6

Ada Gem #76 — In the previous Gem in this series, we saw how to deal with overflow errors, based on source code from Tokeneer. In this Gem, we show how to ensure secure information flow.
This Gem brings us to the end of this series on Tokeneer, and we would like to say a big thank you to the SPARK team at Praxis HIS for providing these resources.
We will now take a break for the holiday period and will return with more Gems on January 11, 2010. Very happy holidays to all Gem readers, wherever you are!

Live Docs

SPARK documentation »

This page gives access to the main SPARK documentation. SPARK Pro provides the foremost language, toolset and design discipline for the engineering of high-assurance software.