Model checking

Kenneth L. McMillan
[ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 13 May 2020

Encyclopedia of Computer Science
John Wiley and Sons Ltd.
Pages 1177-1181
Note(s): survey, model checking, symbolic model checking, partial order reduction, temporal logic
Papers: jhala:compsurv:2009, clarke:cacm:2009

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

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.)

Model checking