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. Actually, this was done with very modest effort: the rewrite of the stabilization code was all done by an intern in two months. Since then, we maintain the resulting code as FLOSS on GitHub, and it has been used for example by the people involved in CAP 2018 project as a prototyping platform.

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. This time, we talk of an autonomous drone operating beyond line of sight. In such a limited timeframe, they achieved both high level of SPARK coverage (portion of the code in SPARK) and high level of automatic proof. They also developed their own agile process around SPARK, using scripts that you can find on this blog. They mostly targeted absence of run-time errors (the Silver level of SPARK assurance) but this is already an impressive feat! In particular they reported about the challenges with proofs of floating-point computations, a topic we have already talked about on this blog.

What's even more interesting for others tempted to do something similar in academia or in industry is that they have published a paper about their experience at SAFECOMP, presented their work at the Frama-C & SPARK Day, and released their code as FLOSS. And of course they are now targeting a more ambitious project to apply the same techniques with SPARK!