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.

ABSTRACT

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.

pdf