Model Checking av Edmund M. Clarke (Carnegie Mellon University) Jr., Orna (Technion) Grumberg, Daniel (Oxford University) Kroening, Doron (Bar Ilan Un

759,-

Kjøp

<b>An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems.</b><p>Model checking is a verification technology that provides an algorithmic means of determining whether an abstract model—representing, for example, a hardware or software design—satisfies a formal specification expressed as a temporal logic formula. If the specification is not satisfied, the method identifies a counterexample execution that shows the source of the problem. Today, many major hardware and software companies use model checking in practice, for verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. This book offers a comprehensive presentation of the theory and practice of model checking, covering the foundations of the key algorithms in depth. </p><p>The field of model checking has grown dramatically since