Current Trends in Hardware Verification and Automated Theorem Proving
This report describes the partially completed correctness proof of the Viper 'block model'. Viper [7,8,9,11,23] is a microprocessor designed by W. J. Cullyer, C. Pygott and J. Kershaw at the Royal Signals and Radar Establishment in Malvern, England, (henceforth 'RSRE') for use in safety-critical applications such as civil aviation and nuclear power plant control. It is currently finding uses in areas such as the de ployment of weapons from tactical aircraft. To support safety-critical applications, Viper has a particulary simple design about which it is relatively easy to reason using current techniques and models. The designers, who deserve…
Mehr
CHF 144.00
Preise inkl. MwSt. und Versandkosten (Portofrei ab CHF 40.00)
V103:
Folgt in ca. 5 Arbeitstagen
Produktdetails
Weitere Autoren: Subrahmanyam, P. a. (Hrsg.)
- ISBN: 978-1-4612-8195-5
- EAN: 9781461281955
- Produktnummer: 13342162
- Verlag: Springer New York
- Sprache: Englisch
- Erscheinungsjahr: 2011
- Seitenangabe: 504 S.
- Masse: H23.5 cm x B15.5 cm x D2.6 cm 756 g
- Auflage: Softcover reprint of the original 1st ed. 1989
- Abbildungen: Paperback
- Gewicht: 756
7 weitere Werke von Graham (Hrsg.) Birtwistle:
Bewertungen
Anmelden