Department of Computer Science and Technology

Technical reports

A mechanized proof of correctness of a simple counter

Avra Cohn, Mike Gordon

July 1986, 95 pages

DOIhttps://doi.org/10.48456/tr-94

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.

Full text

PDF (5.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-94,
  author =	 {Cohn, Avra and Gordon, Mike},
  title = 	 {{A mechanized proof of correctness of a simple counter}},
  year = 	 1986,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-94.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-94},
  number = 	 {UCAM-CL-TR-94}
}