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.

Keywords

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

Authors:

Sections

Buy it now

Buying options

Other ways to access

Table of contents (10 chapters)

Front Matter

Back Matter

About this book