VDM Support in a Generic Reasoning Environment
Peter Lindsay · Australian Software Engineering Conference · 1990
This paper describes our experience using the interactive proof assistant μral (pronounced 'mural') to reason about software designs written In VDM. μral is a generic (logic independent) system and must be configured for particular problem domains. Much of what will be described here amounts to notes on the axiometization of VDM, but many of the lessons learnt undoubtedly apply just as well to other formal methods.