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.
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.
by Yannick Moy in Events – September 15, 2017
The first one-week public SPARK training will occur in Paris in December. You can register online. Registrations will be capped at a dozen participants.
by Yannick Moy in News, Papers and Slides – September 12, 2017
Researcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and slides) which I found extremely interesting.
by Yannick Moy in Formal Verification, Papers and Slides – August 24, 2017
Our good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not used for some time.
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.
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.
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.
by Yannick Moy in News – June 22, 2017
For the first time this year, we're issuing release notes for SPARK Pro in HTML, with code snippets and links to relevant external information.
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.