Simulation as an aid to Verification using the HOL Theorem Prover
The work
| Authors | Albert John Camilleri |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1988 |
| Citekey | camilleri1988simulation |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-150 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| report_number | UCAM-CL-TR-150 |
|---|---|
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-150.html |
|---|
Related
| Distinct from | basin1989verification |
|---|---|
| Distinct from | camilleri1986hardware |
| Distinct from | clocksin1985logic |
| Distinct from | cohn1988correctness |
| Distinct from | gordon1983proving |
| Distinct from | gordon1985why |
| Distinct from | gordon1987hol |
| Distinct from | herbert1988case |
| Distinct from | hunt1994fm8501 |
| Distinct from | joyce1988formal |
| Distinct from | mermet1997survey |
| Distinct from | naylor2015generic |
| Distinct from | winskel1987models |
From bibtex.
Abstract
The HOL theorem proving system, developed by Mike Gordon at the University of Cambridge, is a mechanisation of higher order logic, primarily intended for conducting formal proofs of digital system designs. In this paper we show that hardware specifications written in the HOL logic can be executed to enable simulation as a means for supporting formal proof. Specifications of a small microprocessor are described, showing how HOL logic sentences can be transformed into executable code with minimum risk of introducing inconsistencies. A clean and effective optimisation strategy is recommended to make the executable specifications practical.
A copy is held
pdf, 1.6 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 22:54 UTC |
| Approved by | a person 2026-09-16 09:21 UTC |
Cite it as
@techreport{camilleri1988simulation,
title = {Simulation as an aid to Verification using the HOL Theorem Prover},
author = {Albert John Camilleri},
year = {1988},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
issn = {1476-2986},
}
This record lives at https://refs.drheap.org/camilleri1988simulation/ and will keep doing so.