图灵奖获得者Edmund M.doc

图灵奖获得者 Edmund 访问软件所文章来源:软件研究所发布时间: 2013-04-23 【字号: 小中大】 4月 19 日,应基础软件国家工程研究中心实验室邀请, 2007 年 ACM 图灵奖获得者 Edmund 教授到中科院软件研究所进行访问,并作题为 Turing ’putable Real Numbers and Why They Are Still Important Toda y 的学术讲座,讲座由杨秋松副研究员主持。来自中科院、北京大学、北京信息科技大学等院校的 40 余名老师和学生聆听了报告。 Clarke 教授报告了其研究组在混成系统验证方面的最新工作。安全关键领域的许多应用系统(比如汽车自动机驾驶、民航飞机碰撞检测、高速列车控制以及生物医学系统等), 其本质上是混成系统, 即包含了离散状态变量和根据时间按特定动力学规律变化的连续变量。混成系统的验证具有很高的复杂度, 特别是当描述动力学规律的微分方程为非线性函数( 比如指数、三角函数)时, 该问题是不可判定的。针对该问题, Clarke 教授研究组提出了基于符号化和数字计算的近似判定算法:对于非线性实数理论下的一阶逻辑公式,若非线性函数是 Turing Type 2 可计算的, 则可以给出近似 delta 判定结论,且该 delta 一般非常小,从而保证该结论一般情况下都成立。 Clarke 教授生动报告激起了与会人员的浓厚兴趣,大家对混成系统验证和近似 SMT 判定过程十分关注。报告结束后,与会人员踊跃提问, Clarke 教授就相关问题也一一给予回答。 Clarke 现任美国卡内基梅隆大学计算机科学系教授,是 ACM 和 IEEE 会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉,是模型检验方法的开创者之一, 2007 年获 ACM 图灵奖。 2013 年清华软件日成功举办 2013 年4月 25日至 26日,清华软件日在清华大学 FIT 楼多功能厅举行。本次活动由清华大学软件学院主办,中法联合实验室 LIAMA 协办。本次 TSD 主题是嵌入式软件系统中的相关理论与技术研究热点。清华大学信息科学与技术学院院长、软件学院院长孙家广院士首先就本次活动主题和清华大学在该领域的工作,特别是自主研发的可信嵌入式软件建模与验证工具 Tsmart 做了全面阐述,并给出了该领域的未来发展方向。来自瑞典 Uppsala 大学的 Erik Hagersten 教授以多核环境下的建模与仿真技术做主题报告,针对多核技术给系统建模与仿真带来的新难题,就统计仿真方法、平台无关性能度量和性能变化性分析等技术进行了深入阐述。法国 Pierre et Marie Curie 大学的 Marc Pouzet 教授和 Louis Mandel 博士以同步语言为主题,深入讨论了同步的概念和定义,结合 SCADE 工具介绍了同步语言的特征和验证工具的支持,并阐述了同步语言面临的挑战性问题。来自美国 Carnegie Mellon 大学,同时也是