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 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 Altran 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 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.

SPARK Answers: A series of videos answering the most commonly asked questions about SPARK

SPARK: The proven approach to High Integrity Software. The new 2012 edition of John Barnes' SPARK book is now available! But it now

Knowledge Center

Webinars

SPARK Pro 11 demos

December 10, 2012
Robin Messer highlights the new features released in SPARK Pro 11 including:
- Enhanced Support for Generic Subprograms
- SPARKbridge
- Counter Example Generator: Riposte
- Improvements to the use of Functions in Proof Contexts
- New Proof Statement: Assume
Introducing SPARK 10.1

February 21, 2012
The InSight webinar series continues with a presentation on the new features of the AdaCore/Altran 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.

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 Altran 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.