SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Research Corner - Auto-active Verification in SPARK

by Claire Dross in Formal Verification, Papers and Slides – March 9, 2017

GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. In a paper we are presenting at NASA Formal Methods symposium 2017, we describe how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification.