Providing a formal linkage between MDG and HOL based on a verified MDG system
Formal verification techniques can be classified into two categories: deductive theorem proving and symbolic state enumeration. Each method has complementary advantages and disadvantages. In general, theorem provers are high reliability systems. They can be applied to the expressive formalisms that...
Main Author: | |
---|---|
Published: |
Middlesex University
2002
|
Subjects: | |
Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.392231 |