Please use this identifier to cite or link to this item: http://hdl.handle.net/1880/45721
Title: PROVING A COMPUTER CORRECT IN HIGHER ORDER LOGIC
Authors: Joyce, Jeffrey
Birtwistle, Graham
Keywords: Computer Science
Issue Date: 1-Aug-1985
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 [1] [2]. We have subsequently redone this example in higher order logic using the HOL system [3]. 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.
URI: http://hdl.handle.net/1880/45721
Appears in Collections:Birtwistle, Graham

Files in This Item:
File Description SizeFormat 
1985-208-21.pdf4.6 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.