中国科学院大学 中国科学院大学新闻网

【新闻网讯 记者团 方晨】5月16日，我院爱因斯坦讲席教授托尼(Tony Hoare)来到中关村教学园区S104教室，为科学院的师生作了一场题为《程序正确性的理想模型》的报告。整场报告由中国科学院软件研究所研究员、博士生导师张健先生主持。 托尼教授在报告中向中国科学院的师生详细阐述了他对程序正确性的理想模型——程序验证器的理解。程序验证器能自动的检查程序是否和它的说明是一致的。他指出程序验证器虽然三十年前就提出了，但直到现在还是一个重大的挑战。他提出了近期针对这个挑战所要达到的具体目标——产生一百万行已验证的从重点系统、嵌入式控制、操作系统内核、网络服务应用、桌面程序、开放源码库、代码产生器和编译器等等系统中抽取的代码以及完成这个目标所要达到的具体要求——避免溢出和异常、代码的安全性、内部接口稳定、功能正确性等等方面；介绍了完成这个目标需要的工具以及它能给程序员带来到的种种好处，诸如理性涉及、错误锐减、软件发布周期缩短、演化性和健壮性更好、软件成本降低等等。此外，托尼教授还讲解了程序验证器的理论体系、所需工具和部分实验。 报告结束后，托尼教授还回答了部分同学的提问。 托尼是目前世界上最有影响力的计算机科学家之一，在计算机软件与理论的诸多方面做出了卓越贡献，曾获得了1980年度图灵奖，2000年度京都奖(尖端技术领域)。他早年发明的快速排序算法(Quicksort )。他为了解决程序正确性问题，提出了一种逻辑系统，后来被称为Hoare逻辑。更进一步，为了描述并发系统及其性质，托尼又提出了通信顺序进程(Communicating Sequential Processes, CSP)理论，在学术界产生了深远的影响。 现在，Tony Hoare已从牛津大学退休并就聘于微软公司，正组织“可验证的编译器(The Verifying Compiler)”的国际性项目。该项目被认为是计算机科学界本世纪的一个重大挑战性问题 ( Grand Challenge)。