报告时间:2015-11-20(周五) 15:00
报告地点:九教北307B
报告主题:机械化定理证明以及在形式化验证中的应用
报告主讲:李勇坚 副研究员 中科院软件研究所
【报告人简介】2001获得上海交通大学计算机软件与理论博士学位。从2001年开始至今在中国科学院软件研究所计算机科学国家重点实验室工作,现任副研究员。一直从事硬件形式验证、形式化语义学,协议形式验证的工作,曾经赴澳门联合国大学国际软件研究所参加"实时系统的设计技术"研究计划,已经与美国Portland大学、加拿大Concordia大学、美国Synopsis公司、德国Munich University of Technology大学的同行与学者建立了学术合作与交流联系。主持过国家自然科学基金两项:”符号轨迹计算的形式化语义及模型检测算法研究","基于一阶符号轨迹计算理论的模型检测)。参加过多项国家自然科学重点基金与863项目。在TCS,Formal aspects of computing, and Formal methods in system design 等知名期刊与国际会议上共发表论文20余篇。
【报告简介】机械化定理证明作为重要的形式化验证技术,与模型检测并列为形式化方法的两大支柱技术。本讲座浅谈定理证明的历史、现状,以及问题。对定理证明的基本思想,技术以及在形式化验证应用方面做了入门介绍。