AdaCore Blog

Research Corner - Auto-active Verification in SPARK

by Claire Dross

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. As an example of how far we can go to guide the proof, see the paper we are presenting at NASA Formal Methods symposium 2017. It describes how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification. The code presented in this paper is available as a distributed example in the SPARK github repository and is described in the SPARK user guide (see 'red_black_trees').

Posted in #Formal Verification    #SPARK   

About Claire Dross

Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications. At AdaCore, she works full-time on the formal verification SPARK 2014 toolset.