Handbook of Model Checking

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry.

The editors and authors of this handbook are among the world’s leading researchers in this domain, and the 32 contributed chapters present a thorough view of the origin, theory, and application of model checking. In particular, the editors classify the advances in this domain and the chapters of the handbook in terms of two recurrent themes that have driven much of the research agenda: the algorithmic challenge, that is, designing model-checking algorithms that scale to real-life problems; and the modeling challenge, that is, extending the formalism beyond Kripke structures and temporal logic.

The book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.

Table of Contents

Chapter 1: Introduction to Model Checking
Chapter 2: Temporal Logic and Fair Discrete Systems
Chapter 3: Modeling for Verification
Chapter 4: Automata Theory and Model Checking
Chapter 5: Explicit-State Model Checking
Chapter 6: Partial-Order Reduction
Chapter 7: Binary Decision Diagrams
Chapter 8: BDD-Based Symbolic Model Checking
Chapter 9: Propositional SAT Solving
Chapter 10: SAT-Based Model Checking
Chapter 11: Satisfiability Modulo Theories
Chapter 12: Compositional Reasoning
Chapter 13: Abstraction and Abstraction Refinement
Chapter 14: Interpolation and Model Checking
Chapter 15: Predicate Abstraction for Program Verification
Chapter 16: Combining Model Checking and Data-Flow Analysis
Chapter 17: Model Checking Procedural Programs
Chapter 18: Model Checking Concurrent Programs
Chapter 19: Combining Model Checking and Testing
Chapter 20: Combining Model Checking and Deduction
Chapter 21: Model Checking Parameterized Systems
Chapter 22: Model Checking Security Protocols
Chapter 23: Transfer of Model Checking to Industrial Practice
Chapter 24: Functional Specification of Hardware via Temporal Logic
Chapter 25: Symbolic Trajectory Evaluation
Chapter 26: The mu-calculus and Model Checking
Chapter 27: Graph Games and Reactive Synthesis
Chapter 28: Model Checking Probabilistic Systems
Chapter 29: Model Checking Real-Time Systems
Chapter 30: Verification of Hybrid Systems
Chapter 31: Symbolic Model Checking in Non-Boolean Domains
Chapter 32: Process Algebra and Model Checking