- Chapter 1: What is Model Checking; Clarke, Henzinger, and Veith.
- Chapter 2: Temporal Logic; Piterman.
- Chapter 3: System Modeling; Seshia, Sharygina, and Tripakis.
- Chapter 4: Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking; Bryant.
- Chapter 5: Propositional SAT Solving; Malik and Marques-Silva.
- Chapter 6: Satisfiability Modulo Theories; Barrett and Tinelli. Lectures by Leonardo De Moura: 1, 2, 3
- Chapter 7: Automata Theory and Model Checking; Kupferman.
- Chapter 8: The mu-calculus and Logical Foundations; Bradfield and Walukiewicz.
- Chapter 9: BDD-Based Symbolic Model Checking; Chaki and Gurfinkel.
- Chapter 10: SAT-based Model Checking; Biere and Kroening.
- Chapter 11A: Explicit State Model Checking; Holzmann.
- Chapter 11B: Partial Order Reduction; Peled.
- Chapter 12: Abstraction and Abstraction-Refinement; Dams and Grumberg. Tutorial on BLAST software model checker
- Chapter 13: Compositional Reasoning; Giannakopoulou, Namjoshi, and Pasareanu. Tutorial by Giannakopoulou and Pasareanu
- Chapter 14A: Interpolation: Proofs in the Service of Model Checking; McMillan.
- Chapter 14B: Combining Model Checking and Theorem Proving; Shankar.
- Chapter 15A: Transferring Model Checking Technology to Industry; Kurshan
- Chapter 15B: Hardware Specification Languages; Eisner and Fisman.
- Chapter 16: Software Verification by Predicate Abstraction; Jhala, Podelski, and Rybalchenko.
- Chapter 17: Model Checking Concurrent Software; Gupta, Kahlon, Qadeer, and Touili. Lectures by Arjun Radhakrishna: Part 1; Part 2
- Chapter 18: Combining Model Checking and Data-Flow Analysis; Beyer, Gulwani, and Schmidt.
- Chapter 19: Combining Model checking and Program Testing; Godefroid and Sen. Slides by Sen on CUTE,Slides by Godefroid on SAGE
- Chapter 20: Symbolic Trajectory Evaluation; Melham,
- Chapter 21: Model Checking Procedural Programs; Alur, Bouajjani, and Esparza. Slides from Marktoberdorf Summer School
- Chapter 22: Parametrized Verification; Abdulla, Sistla, and Talupur.
- Chapter 23: Model Checking and Process Algebra; Cleaveland, Roscoe, and Smolka.
- Chapter 24: Model Checking Security Protocols; Basin, Cremers, and Meadows.
- Chapter 25: Graph Games and Reactive Synthesis; Bloem, Chatterjee, and Jobstmann.
- Chapter 26: Symbolic Model Checking in Non-Boolean Domains; Majumdar and Raskin.
- Chapter 27: Verification of Real-Time Systems; Bouyer, Fahrenberg, Larsen, Markey, Ouaknine, and Worrell.
- Chapter 28: Verification of Hybrid Systems; Doyen, Frehse, Pappas, and Platzer.
- Chapter 29: Probabilistic Model Checking; Baier, de Alfaro, Forejt, and Kwiatkowska. Tutorial by Marta Kwiatkowska: Part 1, Part 2
- Syntax-Guided Synthesis

Maintained by Rajeev Alur