SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

SPARK Pro 14.0 Released Today

by Yannick Moy in Language, Formal Verification, News – April 8, 2014

The commercial version of the new SPARK tools, SPARK Pro 14.0, is released today for AdaCore and Altran customers. This is the first official release of this new technology based on the Why3 and Alt-Ergo technologies. A non-commercial GPL licensed version for academics will be released next month. We're happy to show you the results of four years of work!

Two Talks About Automatic Provers

by Claire Dross in Formal Verification, Events – March 25, 2014

The ease of use of the new SPARK technology lies for a large part in the much improved proof automation provided by the use of a state-of-the-art SMT solver at the heart of our technology. If you're interested in this subject, you may want to attend to one of two talks which take place in Saclay near Paris next week.

A Little Exercise With Strings

by Johannes Kanig in Formal Verification – March 19, 2014

I recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function and it's proof are quite simple in the end, the process of obtaining the correct code and the proof was interesting enough to write this blog post.

SPARK 2014 Rationale: Data Dependencies

by Pavlos Efstathopoulos 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.

GNATprove Tips and Tricks: How to Write Loop Invariants

by Yannick Moy in Formal Verification – March 2, 2014

Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants are necessary for various loops, we detail here a methodology for how users can come up with the right loop invariants for their loops. This methodology in four steps allows users to progressively add the necessary information in their loop invariants, with the tool GNATprove providing the required feedback at each step on whether the information provided is sufficient or not.

Case Study for System to Software Integrity Includes SPARK 2014

by Yannick Moy in Formal Verification, Certification, News, Papers and Slides – January 21, 2014

My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.