Model Checking [Hardcover]

Edmund M. Clarke Jr. (Author), Orna Grumberg (Author), Doron A. Peled (Author)

Book Description

ISBN-10: 0262032708 | ISBN-13: 978-0262032704 | Publication Date: January 7, 1999

Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method, which was awarded the 1998 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice to verify real industrial designs, and companies are beginning to market commercial model checkers.The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. In such cases the number of global states can be enormous. Researchers have made considerable progress on this problem over the last ten years.This is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an introduction to the subject and as a reference for researchers.

Editorial Reviews

Review

" Model Checking is bound to be the pre-eminent source for research, teaching, and industrial practice on this important subject. Theauthors include the foremost experts. This is the first trulycomprehensive treatment of a line of research that has gone fromconception to industrial practice in only two decades." R. P. Kurshan , Distinguished Member Technical Staff, Bell Laboratories

About the Author

Edmund M. Clarke, a pioneer of the automated method called Model Checking, is FORE Systems Professor of Computer Science andProfessor of Electrical and Computer Engineering at Carnegie Mellon University, and a winner of the 2007 Turing Award given by the Association for Computing Machinery.

Doron Peled is Professor of Computer Science at the University of Warwick, Coventry, UK.

David M. Newbery is Director of the Department of Applied Economics at Cambridge University. He has been an advisor to the electricity, gas, and rail regulators in various countries.

Product Details

• Hardcover: 314 pages
• Publisher: The MIT Press (January 7, 1999)
• Language: English
• ISBN-10: 0262032708
• ISBN-13: 978-0262032704
• Product Dimensions: 9.2 x 7.3 x 0.9 inches
• Shipping Weight: 1.5 pounds (View shipping rates and policies)
• Average Customer Review: 2.7 out of 5 stars  See all reviews (3 customer reviews)
• Amazon Best Sellers Rank: #678,413 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews

13 of 16 people found the following review helpful:

1.0 out of 5 stars hard to read, July 17, 2005

By 

F. Guerin - See all my reviews
(REAL NAME)   

This review is from: Model Checking (Hardcover)

This book is horribly difficult to read, it is very terse. I found that I could easily follow the things I knew already, but it is not a good book to learn new things from. It is a collection of research results, in a sensible order, but little effort has been made to explain things to the novice. In fact there are research papers which introduce more advanced topics than covered here, and are much easier to read than this book (for example Alur's paper on ATL). It is probably good as a comprehensive reference if you are already familiar with the techniques. It is a shame as there seems to be no other comprehensive book available on model checking. The most accessible introduction remains Manna and Pnueli's "Temporal Verification of Reactive Systems", although it only has one chapter on model checking.

1 of 1 people found the following review helpful:

4.0 out of 5 stars a good reference, September 11, 2007

By 

Husam Abu-Haimed (California, USA) - See all my reviews
(VINE VOICE)    (REAL NAME)   

Amazon Verified Purchase

This review is from: Model Checking (Hardcover)

This is one of the more comprehensive references on model checking. It covers most of the main technqiues used in model checking. It does not cover bounded model checking which became popular after the publication of this book.

The writing style and the explanations in the book could be much better. You just need some patience in reading the book. Overall, I think this book is a useful reference to researchers and practitioners in the field.

This book, however, is NOT for some one who is new to the field. For those who are new to Model Checking and Formal Verification, I strongly recommend "Introduction to Formal Hardware Verification" by Thomas Kropf.

3.0 out of 5 stars classic, but a little out of date, November 16, 2011

By 

happyyang - See all my reviews

This review is from: Model Checking (Hardcover)

This book has long been considered as a must read before doing research in this field. Without doubt, it contains all you need to know about model checking in general. However, it is a little difficult to read for beginners, and also, since it was written 10 years ago, some new advances are not included. Moreover, it puts more emphasis on CTL than LTL, or more "states" than "paths". It is OK, but more difficult to introduce fairness and infinite paths. Personally, I recommend "Principles of Model Checking" by Christel Baier. But still, you may need a copy of this one in your bookshelf.