Towards Deriving Verification Properties
This work tackles a foundational issue in formal methods for software engineers, but it appears incremental as it builds on existing verification assumptions.
The paper addresses the challenge of identifying verification properties in formal software verification, proposing a systematic process for deriving these properties rather than assuming they are known.
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.