程序模型检查器综述  

Survey on Model Checker for Programs

作　　者：林梦香[1] 吴国仕[2] 

机构地区：[1]北京航空航天大学软件开发环境国家重点实验室,北京100083 [2]北京邮电大学软件学院,北京100875

出　　处：《计算机科学》2009年第4期12-15,41,共5页Computer Science

基　　金：863国家重点项目(2007AA010301)资助

摘　　要：模型检查实际程序设计语言编写的程序是近年来程序验证领域的研究热点之一,出现了一批针对C,C++或Java语言的程序模型检查器原型。总结了程序模型检查中的主要问题及相关技术,以是否使用中间建模语言为标准,对现有程序模型检查器进行了分类,并具体地介绍了一些代表性工具中的模型获取及化简技术,最后展望了程序模型检查器未来的研究方向。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 analyzed. Model checkers for programs were classified based on whether an intermediate modeling language is adopted. Methods of model extraction and reduction in some typical tools were introduced. Finally, the future trends of program model checking were discussed.

关 键 词：模型检查 程序模型检查 模型抽取 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]