自动地验证一个系统（硬件、软件等）的行为是否与预期的性质相符合是计算机领域的一个根本问题。模型检验（Model Checking）技术就是针对这个问题提出的解决方案之一。自1981年问世以来，模型检验技术已取得了许多突破性的进展。今天的模型检验技术已广泛应用于硬件工业和通信协议，并在诸如实时嵌入式系统、安全算法等软件验证方面取得了长足的进步，逐渐成为保证计算机系统可信的重要手段。为此，ACM 将 2007 年的图灵奖（Turing Award）授予了对模型检验技术的奠基人美国科学家 Edmund M. Clarke、Allen Emerson 和法国科学家 Joseph Sifakis。
针对“模型检验”，09年3月13日在北京大学理科2号楼2736报告厅，YOCSEF“模型检验”报告会举行。会议由YOCSEF AC委员赵海燕和李晖主持。参加本次报告会的有AC委员陈小武、金蓓弘、王千祥，候任AC委员王涛、袁晓如，委员何万青，以及来自高校、研究单位、企业界和其他感兴趣的人士约100余人。具有80个座位的报告厅内外挤得水泄不通，另有30多人站着听完3个半小时的报告和讨论，其中不乏从外地特地赶来参会的热血学子。
本次报告会邀请了北京大学信息科学与技术学院王捍贫教授、国防科学技术大学计算机学院王戟教授、中国科学院软件研究所计算机科学国家重点实验室张文辉研究员等3位在此领域卓有建树的著名学者，从不同的视角和层次，深入探讨了模型检验技术的研究和应用。
王捍贫教授从模型检验技术产生的背景出发，通过具体的实例简明扼要地介绍了模型检验技术的基本概念、涉及的要素、实施的过程，模型检验技术的各种表示方法及其逻辑基础，同时也强调了模型检验技术在实践中的难点。王戟教授则以“软件模型检验与分析”为题，针对软件模型检验中存在的状态空间爆炸的难点，重点介绍了谓词抽象、切片执行、抽象解释等技术，并展望了模型检验技术与程序分析等技术的结合的发展趋势,以及在并行处理和分布处理等计算平台的支持下提升其在软件模型检验能力方面的前景。张文辉研究员从软件系统模型的状态爆炸问题为出发点，介绍了针对该问题的主要对策的基本原理，包括符号模型检测、抽象方法、合成推理，并重点介绍了相对较新的限界模型检测与验证原理，提出了进一步的研究目标。
三位特邀讲者的演讲前后关联、互为补充，从各个角度为前来参加此次盛会的一百多位听众深入浅出地探讨了模型检验技术及其广泛的应用场景。台下的听众踊跃提问，讲者对所提的问题做了精彩的回答，讨论和交流的气氛非常热烈。报告会结束后，依然有不少听众继续与讲者进行了热烈的讨论。
相关资料链接： 王捍贫-程序验证简介（PDF) 张文辉-模型检测与限界验证（PDF）
（赵海燕供稿）
京公网安备 11010802032778号