Enhance verification using ghost code

Claire Dross - AdaCore

When using tool assistance to verify a software, users are generally faced with two equally complex challenges. How can I express my requirements in the supported language, and how can I convince the tool that my software indeed meets my requirements. Ghost code, or verification specific code, is a construct provided by several formal verification oriented languages to enhance verification. This talk will describe how ghost code can be used in SPARK to enhance both expressivity and provability. Different uses will be exemplified, ranging from simple instances, such as assertions and contracts, to more involved use cases, like model functions and lemma procedures.

Download this presentation

About Claire Dross

Claire has a PhD in computer science specialized in formal proof of programs. She has been working as a software developer and proof expert at AdaCore since 2011. She has been contributing to the the SPARK toolset since the beginning of the 2014 generation.