Verification Technology for VDM: Craft and Automation

Pioneering work in model-oriented specification showed that properties of software could be confirmed or refuted from the early stages of development and be verifiably preserved through design to implementation. As verification technology has evolved, research and innovation have had to balance the insight generated by hand-crafted proof with the benefits of automation. In this paper, we describe QuickCheck, an ‘as-you-specify’ checker for proof obligations in the Vienna Development Method (VDM) Specification Language. Using a classical example of model-oriented specification in VDM, we demonstrate the value of such automated checking of basic proof obligations as a precursor to full machine-assisted proof using the Isabelle theorem prover.