The Formal Verification of the Fairisle ATM Switching Element

The work

AuthorsPaul Curzon
Editors
Typetechreport
Year1994
Citekeycurzon1994formal

Where it appeared

PublisherUniversity of Cambridge Computer Laboratory
Number in seriesUCAM-CL-TR-329
SchoolUniversity of Cambridge Computer Laboratory
Pages113

Identifiers

DOI10.48456/tr-329
report_numberUCAM-CL-TR-329

Access

URLhttps://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-329.html
Landing pagehttps://www.cl.cam.ac.uk/ftp/hvg/papers/LitFabric.ps.gz

Related

Distinct frombillington1987highlevel
Distinct fromcurzon1994formalb
Distinct fromherbert1988case
Distinct fromhopper1986cambridge
Distinct fromwinskel1987relating
Distinct fromwong1993formal

From bibtex.

Abstract

We describe the formal verification of an implementation of the switching element of the fairisle ATM switch. This verification was performed using the HOL90 theorem proving system so is fully machine-checked. We give here all the definitions used in the verification together with the main correctness theorems proved. Fairisle switches are in use in a working network, switching real data. Thus, this work constitutes a realistic formal verification case study.

A copy is held

pdf, 442.3 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-09-16 02:43 UTC
Approved bya person 2026-10-02 10:02 UTC

Filed under

proved-here-used-there the-copy-is-not-the-work you-cannot-patch-silicon

Cite it as

@techreport{curzon1994formal,
  title        = {The Formal Verification of the Fairisle ATM Switching Element},
  author       = {Paul Curzon},
  year         = {1994},
  publisher    = {University of Cambridge Computer Laboratory},
  school       = {University of Cambridge Computer Laboratory},
  pages        = {113},
  doi          = {10.48456/tr-329},
}

This record lives at https://refs.drheap.org/curzon1994formal/ and will keep doing so.