SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

SPARK 16: Shipping CVC4, use two provers by default

by Johannes Kanig in Formal Verification – November 12, 2014

The SPARK toolset is shipped with prover CVC4 in addition to Alt-Ergo. We found that attempting proof first with CVC4, and if this fails, with Alt-Ergo, provides the best compromise between running time and proof result. Therefore, we decided to set this as the default behavior, which can be changed with option --prover.

SPARK Makes History

by Yannick Moy in Formal Verification, Events, Papers and Slides – October 29, 2014

Over its 20+ years of history, SPARK has known quite many cha(lle)nges. Rod Chapman, the "face" of SPARK for many years, wrote his account of this piece of history for a keynote presentation at ITP conference in July 2014. It's quite interesting to read after having just completed this year a major rewrite of the technology.

How to Write Subprogram Contracts

by Yannick Moy in Formal Verification, Design Method – September 30, 2014

GNATprove relies on subprogram contracts to be able to analyze subprograms independently from their callers and callees. But no contracts are compulsory: GNATprove can either generate a contract or use a default value when a contract is not provided by the user. Hence, it is important to know which contracts to write for which verification objectives.

Using SPARK to Prove AoRTE in Robot Navigation Software

by Yannick Moy in Formal Verification, Papers and Slides – August 20, 2014

Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that even NASA has not solved it. Researchers have used SPARK to do precisely that for 3 well-known robot navigation algorithms. Their results will be presented at the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September.

External Axiomatizations: a Trip Into SPARK’s Internals

by Claire Dross in Formal Verification – July 25, 2014

There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the mathematical world, like trigonometry functions), cumbersome (especially if they require concepts that cannot easily be described using contracts, like transitivity, counting, summation...), or simply inefficient, for big and complex data structures like containers for example. In these cases, a user can provide directly a manually written Why3 translation for an Ada package using a feature named external axiomatizations. Coming up with this manual translation requires both a knowledge of the WhyML language and a minimal understanding of GNATprove's mechanisms and is therefore reserved to advanced users.