SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Prove in the Cloud

by Yannick Moy in News – October 18, 2017

We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now experiment live with SPARK without installing first the toolset. Something particularly interesting for academics is that all the code for this widget is open source. So you can setup your own proof server for hands-on sessions, with your own exercises, in a matter of minutes.

SPARK for Agile High-Integrity Development in CACM

by Yannick Moy in News, Papers and Slides – September 25, 2017

Rod Chapman, Neil White and Jim Woodcock are describing the processes that Altran has put in place over the years in its use of agile for developing high-integrity software, where automated formal verification with SPARK plays an important role. Read all about it in the latest issue of Communications of the ACM.

Proving Loops Without Loop Invariants

by Yannick Moy in Formal Verification – July 20, 2017

For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to facilitate writing loop invariants by improving the documentation and the technology in different ways, but writing loops invariants remains difficult sometimes, in particular for beginners. To completely remove the need for loop invariants in simple cases, we have implemented loop unrolling in GNATprove. It turns out it is quite powerful when applicable.

Research Corner - Focused Certification of SPARK in Coq

by Yannick Moy in Papers and Slides – July 18, 2017

The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more complex properties. But the SPARK toolset being itself a complex tool, it is not free of errors. To get confidence in its results, we have worked with academic partners to establish mathematical evidence of the correctness of a critical part of the SPARK toolset. The part on which we focused is the tagging of nodes requiring run-time checks by the frontend of the SPARK technology. This work has been accepted at SEFM 2017 conference.

Applied Formal Logic: Searching in Strings

by Yannick Moy in Dev Projects, Formal Verification – June 29, 2017

A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.

Research Corner - Sensitive Data Sanitization for SPARK

by Yannick Moy in Compilation, Formal Verification, Papers and Slides – June 20, 2017

Well-known SPARK expert and advocate Rod Chapman presented at the latest Ada Europe conference a paper on "Sanitizing Sensitive Data: How to get it Right (or at least Less Wrong...)". Rod's work in the latest years has switched to more security-focused topics it seems, and this work is attacking a subtle problem with new ideas. Definitely worth reading.