QuickCheck for VDM
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912056556388352 |
|---|---|
| author | Battle, Nick Ellyton, Markus Solecki |
| author_facet | Battle, Nick Ellyton, Markus Solecki |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_02046 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | QuickCheck for VDM Battle, Nick Ellyton, Markus Solecki Software Engineering D.2.4; F.3.1 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. |
| title | QuickCheck for VDM |
| topic | Software Engineering D.2.4; F.3.1 |
| url | https://arxiv.org/abs/2410.02046 |