Dr. Dobb's is part of the Informa Tech Division of Informa PLC

This site is operated by a business or businesses owned by Informa PLC and all copyright resides with them. Informa PLC's registered office is 5 Howick Place, London SW1P 1WG. Registered in England and Wales. Number 8860726.

Channels ▼


AdaCore and Altran Praxis Release SPARK Pro 11

The SPARK User Group has announced the release of the SPARK Pro 11 software development and verification environment, providing a step forward for the developers of high-assurance systems.

A number of significant enhancements have been made to the way that functions and proof functions are handled in SPARK Pro 11. These changes will improve project efficiency by eliminating the vast majority of rules that were previously manually encoded. The main changes include a more powerful language for specifying proof functions and the ability to use the functions in any proof context. This greatly simplifies the task of writing and maintaining functional contracts for critical software, providing high-assurance at lower cost.

NOTE: SPARK is 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 that is fast, deep, constructive, and exhibits a low false-alarm rate.

Proof is a powerful technique for achieving high levels of assurance in safety- or security-critical software. However, when performing proofs users typically spend much of their time inspecting undischarged "verification conditions" to determine whether they can indeed be proved.

Included with SPARK Pro 11, Riposte is a new tool that not only determines whether a verification condition is false, but can also generate a counter-example to demonstrate the conditions under which it is false. Riposte is a major improvement to the verification workflow, saving projects a significant amount of time previously spent analyzing improvable verification conditions and providing developers with intuitive explanations. Riposte was developed jointly by Altran Praxis and the University of Bath (UK).

The new assume contract in SPARK Pro 11 allows users to introduce system-level assumptions about programs into their proofs in a clear and concise format. Previously, these assumptions might have been captured by user rules or manual review.

SPARK Pro, a product jointly developed by Altran Praxis and AdaCore, provides a language, toolset, and design discipline for engineering high-assurance software. It combines Altran Praxis' SPARK language and verification tools, with the GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments from AdaCore.

SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset generates evidence for correctness, including proofs of the absence of runtime errors, which can be used to meet the requirements of safety and security certification schemes such as DO-178B, DO-178C, and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C.

Related Reading

More Insights

Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.