SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

VerifyThis Challenge in SPARK

by Yannick Moy in Formal Verification, Events – April 28, 2017

This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.