SPARK is a programming language and a set of tools for building highly reliable software. The SPARK language is a subset of Ada and can be compiled with the GNAT toolchains to a wide range of platforms, including the popular ARM Cortex M3, M4 and M7. The SPARK language also provides specification features, so that the intended behavior of the program can be embedded in the program itself. The SPARK formal verification tool can check that a program does not contain any run-time error, such as buffer or integer overflows, and that the code complies with its specification. We will demonstrate these capabilities on a game of Tetris, whose core game logic has been proved, and which has been ported to several embedded platforms: SAM4S Xplained Pro Evaluation Kit, Pebble Time watch, Unity game engine, Arduboy game platform. We will show in particular that you don’t need any specific mathematical background to achieve such results!
Speakers: Yannick Moy