The HOL Verification of ELLA Designs
The work
| Authors | Richard Boulton; Mike Gordon; John Herbert; John Van Tassel |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1990 |
| Citekey | boulton1990hol |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| School | University of Cambridge Computer Laboratory |
| Pages | 22 |
Identifiers
| DOI | 10.48456/tr-199 |
|---|---|
| report_number | UCAM-CL-TR-199 |
Access
| URL | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-199.ps.gz |
|---|---|
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-199.html |
Related
| Distinct from | cohn1986mechanized |
|---|---|
| Distinct from | lipovski1977hardware |
| Distinct from | vantassel1993femtovhdl |
From bibtex.
Abstract
HOL is a public domain system for generating proofs in higher order predicate calculus. It has been in experimental and commercial use in several countries for a number of years. ELLA is a hardware design language developed at the Royal Signals and Radar Establishment (RSRE) and marketed by Computer General Electronic Design. It supports simulation models at a variety of different abstraction levels. A preliminary methodology for reasoning about ELLA designs using HOL is described. Our approach is to semantically embed a subset of the ELLA language in higher order logic, and then to make this embedding convenient to use with parsers and pretty-printers. There are a number of semantic issues that may affect the ease of verification. We discuss some of these briefly. We also give a simple example to illustrate the methodology.
A copy is held
pdf, 238.3 kB. 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-16 03:04 UTC |
| Approved by | a person 2026-10-02 10:02 UTC |
Filed under
Cite it as
@techreport{boulton1990hol,
title = {The HOL Verification of ELLA Designs},
author = {Richard Boulton and Mike Gordon and John Herbert and John Van Tassel},
year = {1990},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
pages = {22},
doi = {10.48456/tr-199},
}
This record lives at https://refs.drheap.org/boulton1990hol/ and will keep doing so.