Edmund M. Clarke, Orna Grumberg, Doron A. PeledISBN: 0262032708; 9780262032704;
" Model Checking is bound to be the pre-eminent source for research, teaching, and industrial practice on this important subject. The authors include the foremost experts. This is the first truly comprehensive treatment of a line of research that has gone from conception to industrial practice in only two decades." -- R. P. Kurshan, Distinguished Member Technical Staff, Bell Laboratories 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 1999 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice...