QuickCheck for VDM
Nick Battle, Markus Solecki Ellyton
TL;DR
Recent work on a lightweight verification tool for VDM specifications, called QuickCheck, is described, to quickly categorise proof obligations: identifying those that fail with counterexamples, those that are probably provable and those that require deeper analysis.
Abstract
We describe recent work on a lightweight verification tool for VDM specifications, called QuickCheck. The objective of the tool is to quickly categorise proof obligations: identifying those that fail with counterexamples, those that are probably provable and those that require deeper analysis. The paper discusses the design of the tool and its use of pluggable strategies for adding extra checking. We present the results of the tool being used to check a large set of VDM specifications, and suggest future directions.