SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Research Corner - FLOSS Glider Software in SPARK

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!