PROVING A COMPUTER CORRECT IN HIGHER ORDER LOGIC
Date
1985-08-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Description
Keywords
Computer Science