中国计算机学会青年计算机科技论坛
CCF Young Computer Scientists & Engineers Forum
YOCSEF
于2009年3月13日 (星期五) 14:00-17:00
在北京大学理科2号楼2736报告厅
举行报告会，敬请光临
报告会主题
模型检验
自动地验证一个系统（硬件、软件等）的行为是否与预期的性质相符合是计算机领域的一个根本问题。模型检验（Model Checking）技术就是针对这个问题提出的解决方案之一。自1981年问世以来，模型检验技术已取得了许多突破性的进展。今天的模型检验技术已广泛应用于硬件工业和通信协议，并在诸如实时嵌入式系统、安全算法等软件验证方面取得了长足的进步，逐渐成为保证计算机系统可信的有利手段。为此，ACM将 2007 年的图灵奖（Turing Award）授予了对模型检验技术做出了突出贡献的美国科学家Edmund M. Clarke、Allen Emerson 和法国科学家 Joseph Sifakis。本次报告会邀请了国内模型检验领域的3位著名学者，从不同的视角，对模型检验技术的研究和应用等方面进行深入探讨
程 序
13:30 签到
14:00 报告会开始
特邀讲者：王捍贫 博士，北京大学信息科学技术学院教授
演讲题目：模型检验方法简介
特邀讲者：王 戟 博士，国防科技大学计算机学院教授
演讲题目：软件模型检验
特邀讲者：张文辉 博士，中科院软件所计算机科学国家重点实验室研究员
演讲题目：模型检测与限界验证
执行主席：赵海燕 博士，北京大学信息科学技术学院副教授
YOCSEF学术委员会委员
执行主席：李 晖 浙大网新科技股份有限公司品牌总裁助理
YOCSEF学术委员会委员
参加人员：搜索领域相关人士、研究生、媒体及其他有兴趣者
报名咨询Email：ccf-pr@ict.ac.cn; Tel: (010)6256 2503; Fax:6252 7485
模型检验
特邀讲者:王捍贫
 | 京大学信息科学技术学院教授，北京大学软件研究所副所长。CCF理论计算机科学专委会委员。中国离散数学学会副理事长。1993年获北京师范大学基础数学博士学位。主要研究方向为形式化方法、程序语义与验证、逻辑学等。 |
报告提要 为发现计算机系统的错误，美国科学家Edmund M. Clarke、Allen Emerson和法国科学家Joseph Sifakis发明了模型检查技术，用于自动检测计算机硬件和软件中的错误。随着模型检查方法的不断发展，该方法不仅在硬件、协议的验证方面取得巨大成功，近年来在软件验证方面也取得了长足进步。本报告将介绍模型检查的基本原理和方法，包括建模、系统性质的逻辑描述和主要的自动验证方法。
特邀讲者:王戟
 | 国防科学技术大学计算机学院教授、博士生导师，并行与分布处理国防科技重点实验室副主任。中国计算机学会软件工程专业委员会副主任，《中国科学》F辑、《计算机学报》、《软件学报》编委。研究领域是高可信软件、分布计算。先后负责或参加了国家自然科学基金、国家973计划、国家863计划等十余项研究课题，发表论文80余篇。获国家杰出青年科学基金。 |
报告提要 本报告主要介绍软件形式验证中的模型检验技术，包括软件模型检验面临的挑战，目前主要的方法及其应用，以及未来的技术趋势。
特邀讲者:张文辉
 | 中国科学院软件研究所计算机科学国家重点实验室研究员。曾获中国科学院引进国外杰出人才计划资助。主要从事计算机软件形式化方法及相关领域，包括程序的形式验证、逻辑推理、模型检测、以及软件系统设计方法形式化的研究。 |
报告提要 本报告拟从模型检测方法在软件验证应用上的主要难点，即软件系统模型的状态爆炸问题为出发点，重点介绍针对该问题的主要对策的基本原理，包括符号模型检测、抽象方法、合成推理，以及相对较新的限界模型检测与验证原理，并探讨进一步的研究目标。
执行主席:赵海燕
 | 中国计算机学会青年工作委员会委员，YOCSEF学术委员会委员。浙大网新科技股份有限公司总裁助理，兼品牌战略部经理。兼任《中国进出口软件》常务理事，浙江大学MBA联合会常务理事。主要从事企业战略规划，品牌管理，商业模式创新方面的研究。 |
执行主席:李 晖
 | 博士，北京大学信息科学技术学院副教授。YOCSEF学术委员会委员，中国计算机学会高级会员。主要从事软件工程、需求工程、软件复用与构件技术、程序变换和程序设计语言等方面的研究工作。先后主持和参加了包括国家自然科学基金、北京市自然科学基金、国家科技支撑计划、973计划、863计划、中日国际合作项目等在内的多个项目。 |
会场方位图：
京公网安备 11010802032778号
所有评论仅代表网友意见