This book presents current methods for dealing with software reliability, illustrating the advantages and disadvantages of each method. The description of the techniques is intended for a non-expert audience with some minimal technical background. It also describes some advanced techniques, aimed at researchers and practitioners in software engineering. This reference will serve as an introduction to formal methods and techniques and will be a source for learning about various ways to enhance software reliability. Various projects and exercises give readers hands-on experience with the various formal methods and tools.

In addition to describing the individual methods in considerable depth, it also discusses when each method is appropriate and the tradeoffs that are necessary in selecting among them. The different techniques are illustrated by many challenging exercises that can be used in conjunction with state of the art tools. It even tells where to access the tools on the web! I do not know of any other book that covers the same topics with such depth.

The book also describes the process of applying formal methods, starting with modeling and specification, then selecting an appropriate verification technique, and, finally, testing the resulting program. This knowledge is   essential in practice, but is rarely covered in software engineering texts. Most books focus on a particular technique like program testing and do not cover other validation techniques or how several techniques can be used in   combination. Because Doron has made significant contributions to the development of many of the validation techniques described in the book, his insights are particularly important on this critical issue.

The book is appropriate for a wide spectrum of people involved in the development of software. It is particularly appropriate for an upper level undergraduate level course on software reliability or a master's degree course in software engineering. In fact, it is sufficiently well annotated with pointers to other more advanced papers that it can be used as a reference source for software engineers engaged in code validation or by researchers in formal methods.

Having just completed a book on model checking with Doron, I am   immensely impressed with both his talent as a computer scientist and his skill as a writer. I am sure that the present book will be an enormous success. I recommend it with great enthusiasm for anyone who is interested in the problem of software reliability.