Abstract: Model checking real programs coded with modern programming languages get more and more attention. Several program model checkers for C, C＋＋ or Java programming languages were developed. Model checking programs related main problems and basic methods were

Key words: Model checking,Program model checking,Model extraction