AdaCore Labs

SPARK Technology

As part of the HI-Lite project, major enhancements have been made to the SPARK language and toolset. The new SPARK 2014 language is both richer and more flexible, and exploits the Ada 2012 contract-based programming features. 

This will enable greater verification automation and also simplify the development of SPARK 2014 applications. The new toolset that will rely on SPARK 2014 will also provide innovative ways of combining formal verification with testing and will allow SPARK 2014 to be used incrementally in legacy projects. The first commercial release is expected in Q1 2014. For more information please visit

Created on Jun 18th, 2013.  Updated on Jun 18th, 2013.

Yannick Moy

Yannick Moy’s work focuses on software source code analysis, mostly to detect bugs or verify safety/security properties. Yannick previously worked for PolySpace (now The MathWorks) where he started the project C++ Verifier. He then joined 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.

Leave a Comment

Commenting is not available in this channel entry.