Due to the proliferation and pervasiveness of hardware and software entities in everyday life, ascertaining their trustworthiness is of paramount importance. Model checking is a logic-based approach that determines whether the abstract model of an entity conforms to a desired temporal specification. The handbook under review is a collaborative work of 76 leading researchers in the model checking field. This title, which rests upon approximately four decades of research work, covers a wide spectrum of aspects concerning the model checking domain.

The handbook starts with a compelling foreword by Dana Scott, who is widely known for his contributions to automata theory, programming language theory, modal logic, and so on. The handbook is structured in 32 self-contained chapters. The first five chapters describe some core concepts behind model checking. Chapter 1 is a compact introduction to key concepts, algorithmic challenges, modeling challenges, and future research directions of model checking by the editors. Chapter 2 is devoted to temporal specifications, which are grounded in linear temporal logic (LTL), computational tree logic (CTL), and CTL*. Chapter 3 presents the simple modeling language (SML) and Kripke structures to facilitate the construction of abstract models for entities. Chapter 4 concentrates on (i) the relationship between temporal formulas and Büchi automata and (ii) the utilization of an automata-theoretic technique for satisfiability and model checking. Chapter 5 deals with explicit-state model checking, which builds upon automata theoretic structures and search algorithms for asynchronous software verification.

The next ten chapters cover enhancements to the efficiency of explicit-state model checking via a variety of approaches, such as symbolic encodings and abstraction. Chapter 6 is dedicated to the partial order reduction method for alleviating the combinatorial explosion of model checking. Chapter 7 introduces ordered binary decision diagrams (OBDDs), which provide a compact representation of states and transitions. Additionally, OBDDs form the basis of the BDD-based model checking examined in chapter 8. Chapters 9 and 10 discuss the notions of satisfiability (SAT) and SAT-based model checking. Compared to SAT, which relates to the satisfiability of propositional formulas, the satisfiability modulo theories (SMT) problem enables reasoning at a higher level of abstraction through the use of first-order formulas. SMT-based model checking is the focus of chapter 11. Chapters 12 through 15 walk the reader through the other four state explosion alleviating approaches: computational reasoning, abstraction, interpolation, and predicate abstraction.

Subsequent chapters encompass a collection of topics, such as the combination of model checking with various formalisms, the application of model checking, and the notions of real-time model checking and probabilistic model checking. The integration of model checking with data flow analysis, testing, deduction, μ-calculus, and process algebras are covered in chapters 16, 19, 20, 26, and 32, respectively. Chapters 17, 18, and 21 show how different model checking techniques are applied to (i) sequential programs comprising procedure calls; (ii) concurrent programs predicating on pushdown systems (PDs); and (iii) parameterized systems consisting of arbitrary numbers of components. The use of model checking for security protocol analysis, industrial environments, and the hardware industry are explored in chapters 22, 23, 24, and 25. Chapters 27 and 31 present, respectively, the employment of perfect information zero-sum games for generating reactive systems from LTL specifications, and a unified framework underpinned by region algebras and generalized μ-calculus. Chapters 28 through 30 complement the other chapters by examining model checking methods for real-time systems, probabilistic systems, and hybrid systems.

The handbook’s target audience is primarily researchers and graduate students who want to master the technical cores of model checking techniques. The text is encyclopedic in scope and provides an extensive treatment of the model checking domain. Nevertheless, the organization of the handbook could be structured in a better way, for example, by partitioning it into parts that group related chapters together. Besides, model checkers play an integral role in system verification and deserve a separate chapter in the handbook.