2 papers
cs.SE2025
Towards Operation Proof Obligation Generation for VDM
Nick Battle, Peter Gorm Larsen
All formalisms have the ability to ensure that their models are internally consistent. Potential inconsistencies are generally highlighted by assertions called proof obligations, a…
cs.SE2024
QuickCheck for VDM
Nick Battle, Markus Solecki Ellyton
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: identify…