Towards Deriving Verification Properties

TL;DR

This paper discusses a systematic process for deriving verification properties in formal software verification, addressing the common challenge of identifying properties to verify.

Contribution

It introduces a novel process for systematically deriving verification properties, enhancing the applicability of formal methods.

Findings

Proposes a structured approach to property derivation

Addresses the gap in property identification for formal verification

Facilitates broader adoption of formal methods

Abstract

Formal software verification uses mathematical techniques to establish that software has certain properties. For example, that the behaviour of a software system satisfies certain logically-specified properties. Formal methods have a long history, but a recurring assumption is that the properties to be verified are known, or provided as part of the requirements elicitation process. This working note considers the question: where do the verification properties come from? It proposes a process for systematically identifying verification properties.