Formal Specification of the VIPER Microprocessor in HOL
The work
| Authors | C.H. Pygott |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1990 |
| Citekey | pygott1990formal |
Where it appeared
| Publisher | Royal Signals and Radar Establishment |
|---|---|
| Number in series | 90009 |
| School | Royal Signals and Radar Establishment |
Identifiers
| report_number | AD-A242147 |
|---|
Access
| Landing page | https://archive.org/details/DTIC_ADA242147 |
|---|
From bibtex.
Abstract
This report provides a mathematically rigorous specification of the required behaviour of the VIPER microprocessor in the HOL notation (Higher Order Logic) of Cambridge University. This specification has been used as the starting point for a chain of proofs, in an attempt to show that a number of implementations of this specification are indeed correct. This report replaces the early RSRE report 85013, which describes VIPER in the language LCF-LSM (a precursor to HOL).
A copy is held
pdf, 1.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-10-23 00:41 UTC |
| Approved by | a person 2026-10-23 11:26 UTC |
Cite it as
@techreport{pygott1990formal,
title = {Formal Specification of the VIPER Microprocessor in HOL},
author = {C.H. Pygott},
year = {1990},
publisher = {Royal Signals and Radar Establishment},
school = {Royal Signals and Radar Establishment},
}
This record lives at https://refs.drheap.org/pygott1990formal/ and will keep doing so.