A proof of correctness of the Viper microprocessor: the first level
The work
| Authors | Avra Cohn |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1987 |
| Citekey | cohn1987proof |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-104 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| DOI | 10.48456/tr-104 |
|---|---|
| report_number | UCAM-CL-TR-104 |
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-104.html |
|---|
Related
| Distinct from | basin1989verification |
|---|---|
| Distinct from | birtwistle1988vlsi |
| Distinct from | boulton1992hol |
| Distinct from | bryant1991methodology |
| Distinct from | cohn1986mechanized |
| Distinct from | cohn1988correctness |
| Distinct from | cohn1988proof |
| Distinct from | cohn1989notion |
| Distinct from | cullyer1987application |
| Distinct from | cullyer1988implementing |
| Distinct from | gordon1985hol |
| Distinct from | gordon1987hol |
| Distinct from | huang2018instructionlevel |
| Distinct from | hunt1994fm8501 |
| Distinct from | joyce1986proving |
| Distinct from | lee2026formal |
| Distinct from | marino1981general |
| Distinct from | mermet1997survey |
| Distinct from | wong1993formal |
From bibtex.
Abstract
The Viper microprocessor designed at the Royal Signals and Radar Establishment (RSRE) is one of the first commercially produced computers to have been developed using modern formal methods. Viper is specified in a sequence of decreasingly abstract levels. In this paper a mechanical proof of the equivalence of the first two of these levels is described. The proof was generated using a version of Robin Milner’s LCF system.
A copy is held
pdf, 2.2 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 18:27 UTC |
| Approved by | a person 2026-09-23 14:10 UTC |
Filed under
Cite it as
@techreport{cohn1987proof,
title = {A proof of correctness of the Viper microprocessor: the first level},
author = {Avra Cohn},
year = {1987},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
doi = {10.48456/tr-104},
}
This record lives at https://refs.drheap.org/cohn1987proof/ and will keep doing so.