SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Design Method

The Eight Reasons For Using SPARK

by Yannick Moy in Formal Verification, Design Method, Certification, Papers and Slides – September 21, 2015

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.

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.

SPARK 2014 Rationale: Data Dependencies

by in Language, Formal Verification, Design Method – March 18, 2014

Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading the specification of a subprogram we are able to see all of the parameters that the subprogram uses and, in Ada, we also get to know whether they are read, written or both. However, no information regarding the use of global variables is revealed by reading the specifications. In order to monitor and enforce which global variables a subprogram is allowed to use, SPARK 2014 has introduced the Global aspect, which I describe in this post.