The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
This paper describes the experiences of Collins Commercial Avionics and SRI International informally specifying and verifying the microcode for the AAMP5 microprocessor with the PVS verification system. This project was conducted to determine if an industrial microprocessor designed for use in real-time embedded systems could be formally specified at the instruction set and register transfer levels and if formal proofs could be used to prove the microcode correct. The paper provides a brief technical overview, but its emphasis is on the lessons learned in using PVS for an example of this size and the implications for using formal methods in an industrial setting.
@misc{miller1995formal,
title = {Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods},
author = {S.P. Miller and Mandayam K. Srivas},
year = {1995},
pages = {2--16},
doi = {10.1109/wift.1995.515475},
}
This record lives at https://refs.drheap.org/miller1995formal/ and will keep
doing so. It used to be called miller2002formal, and those addresses still resolve to this one.