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.

Head over to our learning site for an interactive introduction to the SPARK programming language and its formal verification tools. You will learn the difference between Ada and SPARK and how to use the various analysis tools that come with SPARK. See the 'Intro to SPARK' course at learn.adacore.com »

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.

Cybersecurity Cover

Read our booklet that summarizes the contribution that the Ada and SPARK languages and AdaCore’s tools can make to develop and verify correct and secure software.

Get our white paper Disruptive Technology for Military Grade Software

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 GNAT Studio 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.

A CWE Compatible Tool

SPARK Pro has been designated as CWE-Compatible by the MITRE Corporation's Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program and can detect a multitude of code weaknesses, including several that are among, or are in the same class as, the CWE’s Top 25 Most Dangerous Software Errors.

SPARK Pro uses advanced proof technology to verify properties of programs written in the SPARK formally analyzable subset of Ada. The tool can prove properties including validity of data/information flow, absence of run-time errors, system integrity constraints (such as safe state transitions), and, for the most critical software, functional correctness with respect to formally specified requirements. SPARK Pro is a sound static analysis tool -- it will detect all violations of a property that it is attempting to verify -- with a very low false alarm rate.

SPARK Pro will prevent or detect the following CWE weaknesses:

CWE weaknessDescription
CWE 119, 120, 123, 124, 125, 126, 127, 129, 130, 131Buffer overflow/underflow
CWE 136, 137Variant record field violation, Use of incorrect type in inheritance hierarchy
CWE 188Reliance on data layout
CWE 190, 191Numeric overflow/underflow
CWE 193Off-by-one error
CWE 194Unexpected sign extension
CWE 197Numeric truncation error
CWE 252, 253Unchecked or incorrectly checked return value
CWE 366Race Condition
CWE 369Division by zero
CWE 456, 457Use of uninitialized variable
CWE 466, 468, 469Pointer errors
CWE 476Null pointer dereference
CWE 562Return of stack variable address
CWE 563Unused or redundant assignment
CWE 682Range constraint violation
CWE 786, 787, 788, 805Buffer access errors
CWE 820Missing synchronization
CWE 821Incorrect synchronization
CWE 822, 823, 824, 825Pointer errors
CWE 835Infinite loop
Partnership 4Inch300Dpi White Transparent

Capgemini Engineering 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

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 »