A Mechanized Proof of Correctness of a Simple Counter

The work

AuthorsAvra Cohn; Mike Gordon
Editors
Typetechreport
Year1986
Citekeycohn1986mechanized

Where it appeared

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

Identifiers

report_numberUCAM-CL-TR-94
ISSN1476-2986

Access

Landing pagehttps://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-94.html

Related

Distinct frombillington1987highlevel
Distinct fromboulton1990hol
Distinct fromcohn1987proof
Distinct fromcohn1988correctness
Distinct fromcohn1989notion
Distinct fromdhingra1988formalising
Distinct fromgordon1983proving
Distinct fromgordon1985formal
Distinct fromgordon1987hol
Distinct fromherbert1988case

From bibtex.

Abstract

The VIPER microprocessor designed at the Royal Signals and Radar Establishment (RSRE) is probably the first commercially produced computer to have been developed using modern formal methods. Details of VIPER are not in the public domain, but the approach used for its verification is fully explained in RSRE Memorandum 3832 entitled "Hardware Proofs using LCF_LSM and ELLA" by John Cullyer and Clive Pygott. In that report, a simple counter is used to illustrate the verification techniques developed by RSRE. Using the same counter, we illustrate the approach to hardware verification developed at Cambridge. This approach is based on the HOL system, an LCF-style proof generator for higher-order logic.

A copy is held

pdf, 5.2 MB. 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-15 22:35 UTC
Approved bya person 2026-09-16 09:22 UTC

Filed under

cohn do-formal-methods-pay gordon the-rare-shared-example you-cannot-patch-silicon

Cite it as

@techreport{cohn1986mechanized,
  title        = {A Mechanized Proof of Correctness of a Simple Counter},
  author       = {Avra Cohn and Mike Gordon},
  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/cohn1986mechanized/ and will keep doing so.