Proving Consistency of VDM models using HOL
Sander D. Vermolen, Jozef Hooman, and Peter Gorm Larsen
Appeared in: Proceedings 25th Symposium on Applied Computing (SAC 2010), pages 2503-2510, ACM, 2010.
Although consistency of formal models is crucial, consistency proofs should not be a large burden to the user. Hence, it is important to have access to efficient proof support which is able to automate a large part of the consistency proofs. We have developed a tool that automatically translates a large subset of VDM and its associated proof obligations, which ensure model consistency, to the theorem prover HOL. In addition, powerful tactics have been
constructed to discard most of the proof obligations automatically.
The application of our approach to four case studies shows that a high degree of automation can be achieved.