Brussels / 4 & 5 February 2017


Yannick Moy

Photo of Yannick Moy

Yannick Moy is the SPARK product manager at AdaCore. He has led the development of the SPARK language and tools since 2010, and he supervised the major technology revision resulting in SPARK 2014. Yannick has presented SPARK in numerous articles, conferences, as well as online (in particular Previously, he worked on software source code analyzers CodePeer, Frama-C and PolySpace Verifier C++. You can contact him at


Title Day Room Track Start End
Prove with SPARK: No Math, Just Code
How to prove key properties of Tetris and run it on ARM Cortex M
Sunday H.2215 (Ferrer) Lightning Talks 12:40 12:55