Model Checking

  • Gerard O’ReganEmail author
Part of the Undergraduate Topics in Computer Science book series (UTICS)


Model checking is an automated technique such that given a finite state model of a system and a formal property (expressed in temporal logic), then it systematically checks whether the property is true of false in a given state in the model.


  1. 1.
    E.M. Clarke, E.A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, in Logic of Programs: Work-Shop, Yorktown Heights, NY, May 1981, vol. 131 of LNCS (Springer, 1981)Google Scholar
  2. 2.
    C. Baier, J. Pieter Katoen, Principles of Model Checking (MIT Press, Cambridge, 2008)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.SQC ConsultingMallow, County CorkIreland

Personalised recommendations