Yannick Moy is Product Manager for the AdaCore SPARK toolsuite, and lead of the Research Directions team at AdaCore. Yannick Moy’s work focuses on software source code analysis, focused on defect detection and formal verification of safety/security properties. Prior to joining AdaCore, Yannick led the development of the C++ Verifier for Polyspace (now part of MathWorks). Thereafter Yannick worked at Inria Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research. Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.