Skip to main content
SpringerLink
Log in
Book cover

Current Trends in Hardware Verification and Automated Theorem Proving

  • Book
  • © 1989

Overview

Editors:
  1. Graham Birtwistle

    1. Department of Computer Science, University of Calgary, Calgary, Canada

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. P. A. Subrahmanyam

    1. AT&T Bell Labs, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (12 chapters)

  1. Front Matter

    Pages i-x
    Download chapter PDF

  2. Correctness Properties of the Viper Block Model: The Second Level

    • Avra Cohn
    Pages 1-91

  3. Formal Verification of the Sobel Image Processing Chip

    • Paliath Narendran, Jonathan Stillman
    Pages 92-127

  4. Specification-driven Design of Custom Hardware in HOP

    • Ganesh C. Gopalakrishnan, Richard M. Fujimoto, Venkatesh Akella, N. S. Mani, Kevin N. Smith
    Pages 128-170

  5. Formal Verification of a Microprocessor Using Equational Techniques

    • R. C. Sekar, M. K. Srivas
    Pages 171-218

  6. OBJ as a Theorem Prover with Applications to Hardware Verification

    • Joseph A. Goguen
    Pages 219-267

  7. Formal Verification in m-EVES

    • Bill Pase, Mark Saaltink
    Pages 268-302

  8. The Interactive Proof Editor An Experiment in Interactive Theorem Proving

    • Brian Ritchie, Paul Taylor
    Pages 303-322

  9. An Overview of the Edinburgh Logical Framework

    • Arnon Avron, Furio Honsell, Ian A. Mason
    Pages 323-340

  10. Automating Recursive Type Definitions in Higher Order Logic

    • Thomas F. Melham
    Pages 341-386

  11. Mechanizing Programming Logics in Higher Order Logic

    • Michael J. C. Gordon
    Pages 387-439

  12. Automated Theorem Proving for Analysis and Synthesis of Computations

    • David R. Musser
    Pages 440-464

  13. What Do Computer Architects Design Anyway?

    • A. L. Davis
    Pages 465-479

  14. Back Matter

    Pages 481-489
    Download chapter PDF
Back to top

Keywords

About this book

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 much credit for the promotion of formal methods, intended from the start that Viper be formally verified. Their idea was to model Viper in a sequence of decreasingly abstract levels, each of which concentrated on some aspect ofthe design, such as the flow ofcontrol, the processingofinstructions, and so on. That is, each model would be a specification of the next (less abstract) model, and an implementation of the previous model (if any). The verification effort would then be simplified by being structured according to the sequence of abstraction levels. These models (or levels) of description were characterized by the design team. The first two levels, and part of the third, were written by them in a logical language amenable to reasoning and proof.

Editors and Affiliations

  • Department of Computer Science, University of Calgary, Calgary, Canada

    Graham Birtwistle

  • AT&T Bell Labs, USA

    P. A. Subrahmanyam

Bibliographic Information

  • Book Title: Current Trends in Hardware Verification and Automated Theorem Proving

  • Editors: Graham Birtwistle, P. A. Subrahmanyam

  • DOI: https://doi.org/10.1007/978-1-4612-3658-0

  • Publisher: Springer New York, NY

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag New York Inc. 1989

  • Softcover ISBN: 978-1-4612-8195-5Published: 17 September 2011

  • eBook ISBN: 978-1-4612-3658-0Published: 06 December 2012

  • Edition Number: 1

  • Number of Pages: X, 489

  • Topics: Computer System Implementation, Electronics and Microelectronics, Instrumentation

Publish with us

Policies and ethics

Back to top

Search

Navigation