FM8501: A Verified Microprocessor
The work
| Authors | Warren A. Hunt, Jr. |
|---|---|
| Editors | |
| Type | misc |
| Year | 1994 |
| Also known as | anon1994fm8501 |
| Citekey | hunt1994fm8501 |
Where it appeared
| Publisher | Springer Berlin Heidelberg |
|---|---|
| Series | Lecture Notes in Computer Science |
| Number in series | 795 |
Identifiers
| DOI | 10.1007/3-540-57960-5 |
|---|---|
| OpenAlex | W1549345379 |
| ISSN | 0302-9743 |
| ISBN | 978-3-540-57960-1 |
Access
| Landing page | https://doi.org/10.1007/3-540-57960-5 |
|---|
Empty on purpose
| abstract, copy |
Related
| Distinct from | angelo1993comparison |
|---|---|
| Distinct from | barrett1987formal |
| Distinct from | basin1989verification |
| Distinct from | camilleri1986hardware |
| Distinct from | camilleri1988simulation |
| Distinct from | cantuortiz1997proof |
| Distinct from | clocksin1985logic |
| Distinct from | cohn1987proof |
| Distinct from | cohn1988correctness |
| Distinct from | davis2013verified |
| Distinct from | gammie2013synchronous |
| Distinct from | hunt2010use |
| Distinct from | hunt2022vwsim |
| Distinct from | toma2006verification |
| Distinct from | winskel1987models |
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-09-15 18:22 UTC |
| Approved by | a person 2026-09-15 21:08 UTC |
Cite it as
@misc{hunt1994fm8501,
title = {FM8501: A Verified Microprocessor},
author = {Warren A. Hunt, Jr.},
year = {1994},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
isbn = {978-3-540-57960-1},
issn = {0302-9743},
doi = {10.1007/3-540-57960-5},
}
This record lives at https://refs.drheap.org/hunt1994fm8501/ and will keep
doing so. It used to be called anon1994fm8501, and those addresses still resolve to this one.