QuickCheck for VDM
Nick Battle, Markus Solecki Ellyton
TL;DR
QuickCheck is a lightweight verification tool for VDM that categorizes proof obligations efficiently, identifying counterexamples, probable proofs, and those needing deeper analysis, with flexible strategies and promising results.
Contribution
The paper introduces QuickCheck, a novel lightweight tool for VDM verification that enhances proof obligation categorization with pluggable strategies.
Findings
Successfully checked a large set of VDM specifications
Effectively categorized proof obligations into different types
Demonstrated potential for future improvements
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Optical Network Technologies