chapters of the book

Each chapter of this handbook is a survey in its own right, and reflects the viewpoint, the notation, and the terminology used by the specialists in the respective research area. The handbook chapters are intended as independent introductions to the state-of-the-art research literature on specific topics rather than as chapters of a monograph.

Introduction to Model Checking

Temporal Logic and Fair Discrete Systems

Modeling for Verification

Automata Theory and Model Checking

Explicit-State Model Checking

Partial-Order Reduction

Binary Decision Diagrams

BDD-Based Symbolic Model Checking

Propositional SAT Solving

SAT-Based Model Checking

Satisfiability Modulo Theories

Compositional Reasoning

Abstraction and Abstraction Refinement

Interpolation and Model Checking

Predicate Abstraction for Program Verification

Combining Model Checking and Data-Flow Analysis

Model Checking Procedural Programs

Model Checking Concurrent Programs

Combining Model Checking and Testing

Combining Model Checking and Deduction

Model Checking Parameterized Systems

Model Checking Security Protocols

Transfer of Model Checking to Industrial Practice

Functional Specification of Hardware via Temporal Logic

Symbolic Trajectory Evaluation

The mu-Calculus and Model Checking

Graph Games and Reactive Synthesis

Model Checking Probabilistic Systems

Model Checking Real-Time Systems

Verification of Hybrid Systems

Symbolic Model Checking in Non-Boolean Domains

Process Algebra and Model Checking