Brussels / 30 & 31 January 2016


CrazyFlie Drone Software in SPARK Ada

An AdaCore intern has rewritten the CrazyFlie drone software, originally in C, into SPARK. In addition to fixing some bugs, this allowed to prove absence of runtime errors. I will present the various technics used to achieve that result, and plan to do a live demo of free fall detection.


Photo of Tristan Gingold Tristan Gingold