Please use this identifier to cite or link to this item:
|Title:||PROVING A COMPUTER CORRECT IN HIGHER ORDER LOGIC|
|Abstract:||Mike Gordon has described the specification and verification of a register-transfer level implementation of a simple general purpose computer using the LCF_LSM hardware verification system  . We have subsequently redone this example in higher order logic using the HOL system . In this paper we present the specification and verification of Gordon's computer as an example of hardware specification and verification in higher order logic.|
|Appears in Collections:||Birtwistle, Graham |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.