图灵奖获得者Edmund M

图灵奖获得者Edmund M.Clarke访问软

件所

文章来源：软件研究所发布时间：2013-04-23 【字号：小中大】4月19日，应基础软件国家工程研究中心实验室邀请，2007年ACM图灵奖获得者Edmund M.Clarke教授到中科院软件研究所进行访问，并作题为Turing’s Computable Real Numbers and Why They Are Still Important Today 的学术讲座，讲座由杨秋松副研究员主持。来自中科院、北京大学、北京信息科技大学等院校的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大学，同时也是2007年图灵奖获得者的Edmund Clarke教授以非线性实数理论的可满足性判定问题做主题报告。非线性实数理论可用于对物理融合系统进行分析和验证，Clarke 教授介绍了他的团队在这一领域的最新研究成果。本场报告同时也是“清华大学巅峰对话”的一部分。学术报告之后，Clarke教授与现场学生就学术问题、科研心得、治学态度等进行了面对面的对话。Clarke教授严谨的科学作风和宽容平和的治学态度赢得了同学们的高度评价。

在学生报告专场，来自清华大学、中科院软件所的多位研究生介绍了自己在模型检测、定理证明和实数理论等方向最新的研究成果。本场活动邀请Edmund Clarke等4位嘉宾为评委，针对学生报告的内容和质量进行打分，并评出了最佳报告人。

清华软件日（简称TSD，Tsinghua software Day）是2011年软件学院为庆祝清华百年校庆所举办的学术研讨活动，今年已经是第三次举办。每次TSD围绕软件理论与系统中的一个前沿主题，邀请世界知名学者做专题报告，并与学生开展面对面的互动交流。本次软件日活动得到了来自清华大学信息学院各院系和中科院、北京大学等北京地区高校百余位学生和科研工作者的高度评价，清华软件日正在成为软件理论与系统领域国际学术交流的平台。