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.
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.
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.
While we are working very hard on semantic analysis in Libadalang, it is already possible to leverage its lexical and syntactic analyzers. A useful example for this is a syntax highlighter.
When things don’t work as expected, developers usually do one of two things: either add debug prints to their programs, or run their programs under a debugger. Today we’ll focus on the latter activity.
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.
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.
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.
The Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it focuses on a control algorithm and a simple serial communications protocol. The iRobot CreateⓇ 2 platform was originally design for STEM education and has great documentation and support - making it very easy to create a control application using Ada. This blog looks at the creation of the project and some cool features of Ada that were learned along the way.
For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.
Updated July 2018
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!
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.
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.
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.
A few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with a freshly brewed cup of coffee every morning. I jokingly said “just give me an espresso machine and I can do the same”. Soon after, the coffee machine is in my office. Now it is time to deliver :)
We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.
After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a copy-paste detector based on Libadalang. It turned out to be both easier than anticipated, and much more efficient and effective than we could have hoped for. In the end, we hope to use this new detector to refactor the codebase of some of our tools, and we expect to integrate it in our IDEs.
This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.
In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.
User friendly strings API In a previous post, we described the design of a new strings package, with improved performance compared to the standard Ada unbounded strings implementation. That post focused on various programming techniques used to make that package as fast as possible.
Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first algorithms that humans devised. So it's quite appealing to try to prove it with an automatic proving toolset like SPARK. It turns out that proving it automatically is not so easy, just like understanding why it works is not so easy. In this post, I am using ghost code to prove correct implementations of the GCD, starting from a naive linear search algorithm and ending with Euclid's algorithm.
This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.
This post has been updated in March 2017 and was originally posted in March 2016.
Two projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the generated JSON files) to either Excel or JSON/text.
Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage
While searching for motivating projects for students of the Real-Time Systems course here at Universitat Politècnica de València, we found a curious device that produces a fascinating effect. It holds a 12 cm bar from its bottom and makes it swing, like an upside-down pendulum, at a frequency of nearly 9 Hz. The free end of the bar holds a row of eight LEDs. With careful and timely switching of those LEDs, and due to visual persistence, it creates the illusion of text... floating in the air!
One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.
GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. In a paper we are presenting at NASA Formal Methods symposium 2017, we describe how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification.
Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)
Earlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical team presented.
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the recording.
At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).
A new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on different machines. Check out this post to see the details.
AdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the only one. At AdaCore, we already have several other tools to process Ada code: the ASIS library, GNAT2XML, the GPS IDE. A realization of the past years, however, has been that we were lacking a unified solution to process code that is potentially evolving, potentially incorrect Ada code. Hence Libadalang.
NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities" in which they single out five approaches which have the potential for creating software with 100 times fewer vulnerabilities than we do today. One of these approaches is formal methods. Among formal methods, the report highlights strong suits of SPARK, and cites SPARK projects as example of mature uses of formal methods. NIST is not the only ones to support the use of SPARK. Editor Bill Wong from Electronic Design has included SPARK in his "2016 Gifts for the Techie". So if your new year's resolutions include software without bugs, have a look at SPARK in 2017.
It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of SPARK Pro, make sure you try it out!
The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My modest Xmas present.
There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.
AdaCore will be hosting a joint webcast next Monday 12th December 2pm ET/11am PT with SPARK experts Yannick Moy and Rod Chapman. Together, they will present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.
Judging for the first annual Make with Ada competition has come to an end and we can now reveal the results.
We report on the creation of the first lemma of a new lemma library on arrays: a lemma on transitivity of the order in arrays.
Customizing build target switches In the first post in this series (Integrate new tools in GPS) we saw how to create new build targets in GPS to spawn external tools via a menu or toolbar button, and then display the output of that tool in its own console, as well as show error messages in the Locations view.
One of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected properties in a modular way. Among the annotations mandated by the SPARK toolset, the hardest to come up with are probably loop invariants. A previous post explains how GNATprove can automatically infer loop invariants for preservation of unmodified record components, and so, even if the record is itself nested inside a record or an array. Recently, this generation was improved to also support the simplest cases of partial array updates. We describe in this post in which cases GNATprove can, or cannot, infer loop invariants for preservation of unmodified array components.
One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.
This blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small plugin might make your daily workflow more convenient by providing toolbar buttons and menus to spawn your tool and parse its output.
One of the interesting aspects of developing software for a bare-board target is that displaying complex application-created information typically requires more than the target board can handle. Although some boards do have amazing graphics capabilities, in some cases you need to have the application on the target interact with applications on the host. This can be due to the existence of special applications that run only (or already) on the host, in particular.
Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.
Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs allowed by the Ravenscar profile. Now it also supports the more relaxed GNAT Extended Ravenscar profile.