We had a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). This year, 139 people registered and around 110-120 actually came. The slides are on the page of the event, under "Slides".

If you did not attend the introduction presentation by Claude Marché, I recommend it. It presents very clearly the common history of Frama-C and SPARK, and the common research topics and joint projects today, that lead to this shared event. As Claude says it in conclusion:

Frama-C and SPARK share not only a common history but

• A will to transfer academic research to the industry of critical software
• Common challenges, approaches, technical solutions

Of particular interest for SPARK users are the presentations of Carl Brandon, Peter Chapin, Martin Becker and Stefan Berghofer:

1. rl Brandon and Peter Chapin presented their Lunar IceCube satellite project that was already mentioned on this blog. It's a 15 million dollar project, with a launch valued 18 million dollar, so Carl and Peter will need every help from SPARK for developing a perfect on-board software! They are trying to open source the core platform on which Lunar IceCube operates, called CubedOS, which isolates applicative threads (14 in their case) from the underlying operating system and Ada runtime. CubedOS is similar to the core Flight System developed at NASA, but it's written in SPARK and the goal is to prove at least correct data flow and absence of run-time errors on the code, possibly even some key properties if time allows.
2. Martin Becker presented his work on a glider software in SPARK. It was a "crazy" project (as he puts it) with such limited timeframe (3 months) and resources (2 persons), so the result is even more impressive. They developed most of the software in SPARK, and achieved both high level of SPARK coverage (portion of the code in SPARK) and automatic proof. They also developed their own agile process around SPARK, using scripts that you can find on this blog.
3. Stefan Berghofer presented his work on formal verification of cryptographic software in SPARK, using the bridge to interactive prover Isabelle for the more complex properties. His team at secunet, together with their colleagues from University of Rapperswil, has been at the forefront of formal program verification with SPARK for many years. Their Muen separation kernel in SPARK is described in this blog post.

I also liked a lot the presentation of Christophe Garion and Jérôme Hugues. They took a fairly large piece of critical software (10,000 sloc in Ada and 15,000 sloc in C), the PolyORB-Hi runtime for distributed software generated from an AADL description, and applied Frama-C on the C version and SPARK on the Ada version to achieve absence of run-time errors and proof of properties. Their conclusion, which matches the initial assessment they did in 2014, is that it is much easier to achieve high assurance through formal program verification in SPARK than in C, mostly because the language really supports it. What I like is that they did exactly what some reviewers keep asking (in my opinion sometimes mistakenly) when we submit articles describing use of SPARK on industrial projects: that we should also submit a comparison with the same goals achieved with other technologies, on programs in other programming languages. This is rarely feasible. Well, they did it!

Unfortunately, the very interesting presentation by Jean-Marc Mota on experiments on the adoption of SPARK at Thales is not available. This blog post presents the levels of software assurance that we defined for SPARK as the result of these experiments.