You simply can't write better code.

SPARK Pro is a language — a formally analyzable subset of Ada 2012 — and toolset that brings mathematics-based confidence to software verification.

Use SPARK Pro to formally define and automatically verify software architectural requirements, and to guarantee a wide range of software integrity properties such as freedom from run-time errors, enforcement of safety properties or security policies, and full functional correctness (compliance with a formally defined specification).

The SPARK Language

The primary design goal of the SPARK language is to provide the foundation for a sound formal verification framework and static analysis toolset. The latest version of the language, SPARK 2014, is based on Ada 2012. It embodies a large subset of Ada 2012, while prohibiting those features which are not amenable to static verification and furthermore can be the source of software defects.

One of the key features of the SPARK language is the ability to be able to express contracts; i.e., behavioral properties that must be implemented correctly by the developer and can be checked by the verification toolset. SPARK 2014 contracts use the same syntax as Ada 2012, thus allowing the developer to express both requirements and implementation within the same language framework. Contracts can be checked at run time using Ada semantics and/or verified statically by the SPARK toolset.

Try SPARK Now

Use SPARK at the right level for you

You can adopt the SPARK methodology through a set of tools built on top of the GNAT Pro Toolsuite. SPARK Pro is the most complete toolset for SPARK. SPARK Discovery (included in GNAT Pro) is a reduced toolset that performs the same analyses as SPARK Pro but only comes with one automatic prover instead of three. Other advantages of SPARK Pro over SPARK Discovery include integration of the CodePeer static analyzer proof technology, generation of counterexamples for failed proofs, support for programs using modular arithmetic or floating-point arithmetic, and a lemma library for more difficult proofs.

Stone

Start benefiting from the stronger guarantees provided by the SPARK language restrictions.

Available with SPARK Discovery and SPARK Pro

Bronze

Use data flow analysis and information flow analysis to eliminate broad classes of errors, such as reading an uninitialized variable.

Available with SPARK Discovery and SPARK Pro

Silver

Guarantee that your software is free from run-time errors.

Available with SPARK Discovery and SPARK Pro

Gold

Use proofs to guarantee critical properties of your software.

Available with SPARK Pro

Platinum

Prove that your most critical code satisfies its functional specifications.

Available with SPARK Pro

When software failure is unacceptable, ultra-high reliability can be attained at the same level of effort as traditional testing-based methods.

Through the use of formal methods, SPARK Pro  prevents, detects and eliminates defects early in the software lifecycle with mathematics-based assurance. It also helps reduce delivery costs and timescales. The SPARK language and tools have a proven track record in the most demanding safety-critical and high-security systems. They are easily learned by software professionals and do not require a background in formal methods. Experience in projects such as Tokeneer shows that formal methods can achieve ultra-high reliability in a cost-effective manner.

SPARK Pro offers an integrated approach to the entire software design and verification lifecycle.

SPARK Pro brings software specification, coding, testing, and unit verification by proof within a single integrated framework. Verification goals that would otherwise have to be achieved by diverse techniques such as manual review can be met by applying the SPARK toolsuite, and reports can be generated to satisfy certification requirements.

The SPARK programming language can be used both for new development efforts and incrementally in existing projects in other languages (such as C and C++). It can be combined with testing in an approach known as hybrid verification.

Integrated Approach

Features

Integration in IDEs

The SPARK Pro toolset is fully integrated with the GPS and GNATbench IDEs, so that errors and warnings can be displayed within the same environment as the source code thereby providing a smoother workflow for the developer. Alternatively, the tools can be run in command-line mode, for example to generate the reports required for certification evidence.

Data Flow Analysis

SPARK Pro detects common programming errors that can be the cause of insecurities or incorrect behavior, including references to uninitialized variables. Advanced data flow analysis can be used to check that access to global variables conforms to contracts specified by a software architect, thereby ensuring that the software conforms to its architectural design.

Information Flow Analysis

For more critical applications, dependency contracts can be specified to constrain the information flow allowed in a program (how global variables and formal parameters are used by a subprogram). Violations of these contracts - potentially representing violations of safety or security policies - can then be detected even before the code is compiled.

Absence of Run-Time Exceptions

SPARK Pro can check that a program is free from run-time exceptions such as divide-by-zero, numeric overflow, buffer overflow or out-of-bounds array indices. The mathematical proof system on which SPARK Pro is based guarantees that this analysis is sound, so that even before a program is executed or tested a large class of potentially hard-to-detect errors can be eliminated from your software.

Property Checking

For more critical applications, key safety or security properties can be expressed in the same contract notation as is used in Ada 2012 (for example, subprogram pre- and postconditions). Using a proof system that is mathematically sound, the SPARK Pro toolset can automatically check whether a program will satisfy these properties for all possible inputs and execution paths - as if the program had been exhaustively tested but without ever having to compile or run the code.

Functional Correctness

With its extended contract language, SPARK allows a comprehensive formal specification of a program’s required functional behavior; i.e., a specification of its Low-Level Requirements. The SPARK Pro tools will attempt to prove that a program meets its functional specification, thus providing the highest possible level of assurance for the correct behavior of critical systems.

Partnership 4Inch300Dpi White Transparent

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.

Customer Projects: SPARK Pro

  • TOYOTA ITC

    High-Reliability Vehicle Component Research Project

    TOYOTA InfoTechnology Center (ITC) Japan selected the SPARK language and SPARK Pro toolset for a research project to develop a vehicle component implementation that can be proven to be free of run-time errors.

  • Secunet

    Multi-Level Security Workstation

    To develop a robust multi-level security workstation, Secunet Security Networks chose the SPARK Pro development environment. The security station concurrently handles information of different security domains, maintains confidentiality and integrity of all processed data, and enforces Multiple Independent Levels of Security (MILS) on a single hardware platform.

  • NATS

    iFACTS - Air Traffic Management System

    iFACTS is the future of air traffic control. The combination of Praxis’ experience in critical systems engineering and the high integrity of SPARK Ada enabled the development of this vitally important and sophisticated system.

  • Rockwell Collins

    Cross Domain Guard for Military Tactical Systems

    Rockwell Collins successfully used SPARK Pro and GNAT Pro High-Security in the development of the SecureOne™ Guard, a high assurance cross domain guard for military tactical systems.

  • Vermont Technical College

    Flight Software for Lunar IceCube Satellite

    The GNAT Pro and SPARK language toolsets have been selected for the Lunar IceCube project by Vermont Technical College. Lunar IceCube is a 6-Unit CubeSat mission sponsored by NASA through their NextSTEP initiative. The mission will prospect for water and other lunar volatiles in all forms (solid, liquid, and vapor) from a highly elliptical orbit with a low point of 100 kilometers (60 miles) where the data will be gathered, and a high point of 5,000 kilometers (3,100 miles). 

View all customer projects »

Expert Support

Integral to every one of our products are the consulting and support services we provide to our customers. While every company says they offer excellent support, for us it‘s a critical part of our business model and something we take very seriously.

Learn more about Expert Support »