« BACK TO PROGRAM
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.