Related Work

This is a good survey of model checking that lays out the main concepts and why they matter:

• specification
  • temporal logic
    • branching time logic (BTL)
      • computation tree logic (CTL)
    • linear temporal logic (LTL)
  • automata-based specification and verification
• scaling and performance of implementation
  • the state explosion problem
  • symbolic model checking
  • exploitation of symmetry
  • partial order-based reductions
  • abstraction and compositional methods
    • abstraction
    • compositional methods

While this all remains very relevant, this article is from 2003 and the most recent citation is from 1998 and most of them are from the ’80s so this survey needs to be supplemented with an update on the last 20 years. (It also doesn’t say much about how a model checker works internally.)

Notes related to Model checking

Model checking