图灵奖获得者EdmundM.doc

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