Skip to main content
SpringerLink
Log in
Book cover

Symbolic Model Checking

  • Book
  • © 1993

Overview

Authors:
  1. Kenneth L. McMillan

    1. Carnegie Mellon University, Australia

    View author publications

    You can also search for this author 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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.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 (10 chapters)

  1. Front Matter

    Pages i-xvii
    Download chapter PDF

  2. Introduction

    • Kenneth L. McMillan
    Pages 1-9

  3. Model Checking

    • Kenneth L. McMillan
    Pages 11-24

  4. Symbolic Model Checking

    • Kenneth L. McMillan
    Pages 25-60

  5. The SMV System

    • Kenneth L. McMillan
    Pages 61-85

  6. A Distributed Cache Protocol

    • Kenneth L. McMillan
    Pages 87-112

  7. Mu-Calculus Model Checking

    • Kenneth L. McMillan
    Pages 113-128

  8. Induction and Model Checking

    • Kenneth L. McMillan
    Pages 129-141

  9. Equivalence Computations

    • Kenneth L. McMillan
    Pages 143-151

  10. A Partial Order Approach

    • Kenneth L. McMillan
    Pages 153-177

  11. Conclusion

    • Kenneth L. McMillan
    Pages 179-181

  12. Back Matter

    Pages 183-194
    Download chapter PDF
Back to top

Keywords

About this book

Formal verification means having a mathematical model of a system, a language for specifying desired properties of the system in a concise, comprehensible and unambiguous way, and a method of proof to verify that the specified properties are satisfied. When the method of proof is carried out substantially by machine, we speak of automatic verification. Symbolic Model Checking deals with methods of automatic verification as applied to computer hardware.
The practical motivation for study in this area is the high and increasing cost of correcting design errors in VLSI technologies. There is a growing demand for design methodologies that can yield correct designs on the first fabrication run. Moreover, design errors that are discovered before fabrication can also be quite costly, in terms of engineering effort required to correct the error, and the resulting impact on development schedules. Aside from pure cost considerations, there is also a need on the theoretical side to provide a sound mathematical basis for the design of computer systems, especially in areas that have received little theoretical attention.

Authors and Affiliations

  • Carnegie Mellon University, Australia

    Kenneth L. McMillan

Bibliographic Information

  • Book Title: Symbolic Model Checking

  • Authors: Kenneth L. McMillan

  • DOI: https://doi.org/10.1007/978-1-4615-3190-6

  • Publisher: Springer New York, NY

  • eBook Packages: Springer Book Archive

  • Copyright Information: Kluwer Academic Publishers 1993

  • Hardcover ISBN: 978-0-7923-9380-1Published: 31 July 1993

  • Softcover ISBN: 978-1-4613-6399-6Published: 23 October 2012

  • eBook ISBN: 978-1-4615-3190-6Published: 06 December 2012

  • Edition Number: 1

  • Number of Pages: XVII, 194

  • Topics: Circuits and Systems, Electrical Engineering, Theory of Computation

Publish with us

Policies and ethics

Back to top

Search

Navigation