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.
by Yannick Moy
in Formal Verification, News
– June 15, 2017
SPARK Discovery GPL 2017 is out! With more automation of proofs, new modes of user interaction, support for type invariants. Note that the optional provers CVC4 and Z3 are no longer distributed with SPARK Discovery GPL 2017, and should be installed separately.
by Yannick Moy
in Dev Projects, Formal Verification, Papers and Slides
– June 11, 2017
Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove absence of run-time errors (no buffer overflows, not division by zero, etc.) on such code. The researchers Martin Becker and Emanuel Regnath have raised the bar by developing the code for the autopilot of a small glider in SPARK in three months only. Their paper and slides are available, and they have released their code as FLOSS for others to use/modify/enhance!
by Yannick Moy
in Formal Verification, Papers and Slides
– June 8, 2017
It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.
by Yannick Moy
in News, Papers and Slides
– June 2, 2017
The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). Here is a summary of what was interesting for SPARK users. We also point to the slides of the presentations.
by Yannick Moy
in Formal Verification, Papers and Slides
– May 27, 2017
While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.