The Beginning of Model Checking: A Personal Perspective.

Model checking provides an automated method for verifying concurrent systems. Correctness specifications are given in temporal logic. The method hinges on an efficient and flexible graph-theoretic reachability algorithm. At the time of its introduction in the early 1980΄s, the prevailing paradigm for verification was a manual one of proof-theoretic reasoning using formal axioms and inference rules oriented towards sequential programs. The need to encompass concurrent programs, the desire to avoid the difficulties with manual deductive proofs, and the small model theorem for temporal logic motivated the development of model checking. [ABSTRACT FROM AUTHOR]