SPARK is a programming language and a set of tools for building highlyreliable software. The SPARK language is a subset of Ada and can be compiledwith the GNAT toolchains to a wide range of platforms, including the popularARM Cortex M3, M4 and M7. The SPARK language also provides specificationfeatures, so that the intended behavior of the program can be embedded in theprogram itself. The SPARK formal verification tool can check that a programdoes not contain any run-time error, such as buffer or integer overflows, andthat the code complies with its sphttps://178.248.245.19/mfc/main.cgi#ecification. We will demonstrate thesecapabilities on a game of Tetris, whose core game logic has been proved, andwhich has been ported to several embedded platforms: SAM4S Xplained ProEvaluation Kit, Pebble Time watch, Unity game engine, Arduboy game platform.We will show in particular that you don’t need any specific mathematicalbackground to achieve such results! Room: H.2215 (Ferrer) Scheduled start: 2017-02-05 11:40:00