Model Checking: Algorithmic Verification and Debugging. - Clarke, Edmund M.; Emerson, E. Allen; Sifakis, Joseph (Communications of the ACM, 2009)
The authors discuss their formulation of the process of model checking and its historical background. Mathematical logic is used in model checking to confirm that computer program behavior conforms to the correct specifications. While the Floyd-Hoare style deductive verification method was used since the 1960s, it was not useful for large programs. Model checking was devised using temporal logic (TL) that describes change over time. Debugging, correctness, expressiveness, efficiency and accounting for architectures and their features in model checking are detailed.