Hardware Verification using Higher-Order Logic
The work
| Authors | Albert Camilleri; Mike Gordon; Tom Melham |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1986 |
| Citekey | camilleri1986hardware |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| Number in series | UCAM-CL-TR-91 |
| School | University of Cambridge Computer Laboratory |
Identifiers
| report_number | UCAM-CL-TR-91 |
|---|---|
| ISSN | 1476-2986 |
Access
| Landing page | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.html |
|---|
Related
| Distinct from | aagaard1999are |
|---|---|
| Distinct from | basin1989verification |
| Distinct from | basin1991formally |
| Distinct from | bryant1987cosmos |
| Distinct from | bryant1991methodology |
| Distinct from | camilleri1988simulation |
| Distinct from | cardelli1982algebraic |
| Distinct from | clocksin1985logic |
| Distinct from | cohn1988correctness |
| Distinct from | dhingra1988formalising |
| Distinct from | fugger2016unfaithful |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1985hol |
| Distinct from | gordon1985why |
| Distinct from | gordon1987hol |
| Distinct from | herbert1988case |
| Distinct from | hunt1994fm8501 |
| Distinct from | joyce1987hardware |
| Distinct from | leeser1988reasoning |
| Distinct from | mateescu2020modeling |
| Distinct from | melham1987abstraction |
| Distinct from | melham1988using |
| Distinct from | melham1990formalizing |
| Distinct from | paulson2018michael |
| Distinct from | traub1986formal |
| Distinct from | winskel1987models |
| Distinct from | winskel1987relating |
| Distinct from | winskel1988compositional |
| Distinct from | zhao2026formally |
From bibtex.
Abstract
The Hardware Verification Group at the University of Cambridge is investigating how various kinds of digital systems can be verified by mechanised formal proof. This paper explains our approach to representing behaviour and structure using higher-order logic. Several examples are described, including a ripple-carry adder and a sequential device for computing the factorial function. The dangers of inaccurate models are illustrated with a CMOS exclusive-or gate.
A copy is held
pdf, 1.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 21:57 UTC |
| Approved by | a person 2026-09-16 09:23 UTC |
Cite it as
@techreport{camilleri1986hardware,
title = {Hardware Verification using Higher-Order Logic},
author = {Albert Camilleri and Mike Gordon and Tom Melham},
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/camilleri1986hardware/ and will keep doing so.