Technical reports

A proof of correctness of the Viper microprocessor: the first level

Avra Cohn

January 1987, 46 pages

DOI: 10.48456/tr-104

Abstract

The Viper microprocessor designed at the Royal Signals and Radar Establishment (RSRE) is one of the first commercially produced computers to have been developed using modern formal methods. Viper is specified in a sequence of decreasingly abstract levels. In this paper a mechanical proof of the equivalence of the first two of these levels is described. The proof was generated using a version of Robin Milner’s LCF system.

Full text

PDF (2.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-104,
  author =	 {Cohn, Avra},
  title = 	 {{A proof of correctness of the Viper microprocessor: the
         	   first level}},
  year = 	 1987,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-104.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-104},
  number = 	 {UCAM-CL-TR-104}
}