@inbook {IOPORT.01698866,
    author       = {Holzmann, Gerard J.},
    title        = {Software model checking.},
    year         = {2001},
    booktitle    = {Engineering theories of software construction. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 25 -- August 6, 2000},
    isbn         = {1-58603-172-4},
    pages        = {309-355},
    publisher    = {Amsterdam: IOS Press; Tokyo: Ohmsha},
    abstract     = {Summary: We review the automata-theoretic verification method and propositional linear temporal logic, with specific emphasis on their potential application to distributed software verification. An important issue in software verification is the establishment of a formal relation between the concrete, implementation-level, software application and the abstract, derived, automata-model that is the subject of the actual verification. In principle one can either attempt to derive an implementation from a verified abstract model, using refinement techniques, or one can attempt to derive a verification model from an implementation, using systematic abstraction techniques. The former method has long been advocated, but has not received much attention in industrial practice. The latter method, deriving abstract models from concrete implementations guided by explicitly stated correctness requirements, has recently begun to show considerable promise. We discuss it in detail.},
    identifier   = {01698866},
}