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图灵奖。

Edmund M.Clarke教授作报告

讲座现场