SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Research Corner - SPARK on Lunar IceCube Micro Satellite

by Yannick Moy in News, Papers and Slides – November 9, 2016

Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.

The Most Obscure Arithmetic Run-Time Error Contest

by Yannick Moy in Formal Verification – September 22, 2016

Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course, everyone knows about overflow checks and range checks (although many people confuse them) and division by zero. After all, these are typical errors that do show up in programs, so programmers are aware that they should keep an eye on these. Or do they?

Automatic Generation of Frame Conditions for Record Components

by Claire Dross in Formal Verification – July 26, 2016

Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the preservation of variables which are not modified in the loop need not be mentioned in the invariant, it is in general necessary to state explicitly the preservation of unmodified object parts, such as record fields or array elements. These preservation properties form the loop’s frame condition. As it may seem obvious to the user, the frame condition is unfortunately often forgotten when writing a loop invariant, leading to unprovable checks. To alleviate this problem, the GNATprove tool now generates automatically frame conditions for preserved record components. In this post, we describe this new feature on an example.

Make with SPARK

by Yannick Moy in Events – June 20, 2016

AdaCore has launched the "Make with Ada" competition just today: teams of up to four have until September 30th to submit projects in Ada or SPARK which will be evaluated by a jury of four personalities of the embedded software domain: Bill Wong, Jack Ganssle, Dick Selwood and Cyrille Comar. The 5 prices range from a Crazyflie nano-copter to 5000 euros.

SPARK GPL 2016 Is Available

by Yannick Moy in News – June 1, 2016

The annual releases of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, this means support of concurrency with Ravenscar, generation of counterexamples and better proof automation. Enjoy!