SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014


SPARK 2014 Rationale: Support for Ravenscar

by Yannick Moy in Language, Formal Verification – November 23, 2015

As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. In this post, I revisit the example given by Pavlos to show SPARK features and GNATprove analysis in action.

SPARK 2016 supports Ravenscar!

by in Language, Formal Verification – November 12, 2015

The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races will occur and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice.

SPARK 2014 Rationale: Variables That Are Constant

by in Language, Formal Verification – September 22, 2015

The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...

SPARK 2014 Rationale: Type Predicates

by Yannick Moy in Language, Formal Verification – July 24, 2015

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

SPARK 2014 Rationale: Functional Update

by Yannick Moy in Language, Formal Verification – January 21, 2015

While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently express how record and array objects are modified by a procedure. A special attribute Update is defined in SPARK to make it easy to express such properties.

SPARK 2014 Rationale: Object Oriented Programming

by Yannick Moy in Language, Formal Verification – January 14, 2015

Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known statically. The standard for civil avionics certification has recognized this specific problem, and defines a specific verification objective called Local Type Consistency that should be met with one of three strategies. SPARK allows using one of these strategies, by defining the behavior of an overridden subprogram using a special class-wide contract and checking that the behavior of the overriding subprogram is a suitable substitution, following the Liskov Substitution Principle.

SPARK 2014 Rationale: Ghost Code

by Yannick Moy in Language, Formal Verification – January 7, 2015

A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. If you're careful or lucky enough, the additional code you write will not impact the program being verified, and it will be removed during compilation, so that it does not inflate binary size or waste execution cycles. SPARK provides a way to get these benefits automatically, by marking the corresponding code as ghost code, using the new Ghost aspect.