Proving a computer correct in higher order logic
The work
| Authors | Jeff Joyce; Graham Birtwistle; Mike Gordon |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1986 |
| Citekey | joyce1986proving |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-100 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| report_number | UCAM-CL-TR-100 |
|---|---|
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-100.html |
|---|
Related
| Distinct from | burch1994automatic |
|---|---|
| Distinct from | cantuortiz1997proof |
| Distinct from | cohn1987proof |
| Distinct from | cohn1988correctness |
| Distinct from | gammie2013synchronous |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1983proving |
| Distinct from | gordon1985formal |
| Distinct from | gordon1985hol |
| Distinct from | gordon1985why |
| Distinct from | huang2018instructionlevel |
| Distinct from | joyce1987hardware |
| Distinct from | joyce1988formal |
| Distinct from | joyce1990multilevel |
| Distinct from | kumar1996formal |
| Distinct from | lee2026formal |
| Distinct from | melham1993higher |
| Distinct from | xue2024using |
From bibtex.
Abstract
Technical Report No. 42, 'Proving a Computer Correct using the LCF_LSM Hardware Verification System', describes the specification and verification of a register-transfer level implementation of a simple general purpose computer. The computer has a microcoded control unit implementing eight user level instructions. We have subsequently redone this example in higher order logic using the HOL hardware verification system. This report presents the specification and verification of Gordon's computer as an example of hardware specification and verification in higher order logic. The report describes how the structure and behaviour of digital circuits may be specified using the formalism of higher order logic. The proof of correctness also shows how digital behaviour at different granularities of time may be related by means of a temporal abstraction. This report should be read with Technical Report No. 68, 'HOL, A Machine Oriented Formulation of Higher Order Logic', which describes the logic underlying the HOL hardware verification system.
A copy is held
pdf, 3.3 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 21:17 UTC |
| Approved by | a person 2026-09-16 09:30 UTC |
Cite it as
@techreport{joyce1986proving,
title = {Proving a computer correct in higher order logic},
author = {Jeff Joyce and Graham Birtwistle and Mike Gordon},
year = {1986},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
}
This record lives at https://refs.drheap.org/joyce1986proving/ and will keep doing so.