SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Research Corner - Focused Certification of SPARK in Coq

by Yannick Moy in Papers and Slides – July 18, 2017

The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more complex properties. But the SPARK toolset being itself a complex tool, it is not free of errors. To get confidence in its results, we have worked with academic partners to establish mathematical evidence of the correctness of a critical part of the SPARK toolset. The part on which we focused is the tagging of nodes requiring run-time checks by the frontend of the SPARK technology. This work has been accepted at SEFM 2017 conference.