转自http://news.ustc.edu.cn/xwbl/201110/t20111009_120986.html

我校研究论文被POPL录用 为大陆研究机构首篇被录用论文 2011-10-09 日前，中科大－耶鲁高可信软件联合研究中心梁红瑾、冯新宇和付明的论文“一种用于验证并发程序变换的基于依赖-保证的模拟关系”（A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations）被第39届编程语言原理国际会议（ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages，简称POPL）录用。此前，中国大陆尚无任何单位以第一作者单位的身份在POPL上发表过论文，中国科大是第一个以第一单位在POPL上发表论文的高校和科研院所。

POPL是编程语言领域历史最久、水平最高的国际会议，它是讨论编程语言和编程系统最新突破的最主要论坛，内容涵盖编程语言的理论、编程语言的设计、编译器技术、程序分析、程序验证、可信软件等众多研究领域。国际期刊和会议的各种分区方法都把POPL放在该领域的最高区域中。

论文第一作者梁红瑾是中国科大计算机科学与技术学院博士一年级学生，她与冯新宇教授等的论文提出了一种验证并发程序变换的一般方法，首次将并发程序逻辑中的依赖-保证条件（rely-guarantee conditions）引入到传统的程序模拟关系（simulation）中，成功地解决了对验证提供模块化支持的难题，并将这种方法应用于编译优化、并发数据结构的实现和并发垃圾收集等算法的正确性验证。审稿人对论文的贡献给予了充分肯定，他们分别指出：“我感到这篇文章很吸引人。结合模拟关系与依赖-保证推理的想法看起来很不错，而且我在别处都没有见过……这项工作能提供一种漂亮的统一理论，用于验证并发程序变换。”“并发系统的精化问题的研究非常具有挑战性，这篇文章则向这个领域迈出了很好的一步。”“一个能够同时支持运行时系统验证和编译器验证的逻辑将非常有用。这篇文章展示了这样一个逻辑，并且看起来是一种非常普适的、自然的方法。”

作为联合研究中心的研究进入国际一流水平的又一体现是，联合研究中心邵中教授（我校大师讲席教授）和冯新宇教授被介绍国际新兴技术的期刊列为国际上从事新兴技术“防崩溃代码”（Crash-Proof Code）的主要研究人员。防崩溃代码是美国麻省理工学院主办的、颇具影响力的Technology Review杂志（中文版名字为《科技创业》）今年第6期评选出的2011年度十大新兴技术之一。这项技术是指用逻辑推理的方法来进行程序验证，以构造高可信的安全攸关软件。《科技创业》主要介绍了澳大利亚国家信息与通信技术研究中心（NICTA）2009年完成的对可以实际应用的操作系统内核seL4的验证。《科技创业》在有关这项技术的报导中提到，从事这方面研究的还有我校冯新宇教授、微软Redmond研究院Chris Hawblitzel研究员和耶鲁大学邵中教授。

NICTA的研发主要展示验证大型系统软件的可行性。他们验证了seL4的大部分代码，但由于相关理论和技术的欠缺，不得不放弃对一些最底层的关键代码的验证，包括底层部分C代码和600行汇编代码，因而可靠性保证尚不够彻底。邵中教授和冯新宇教授的研究则主要针对系统软件验证中的关键理论和技术。他们带领联合研究中心的研究人员等在2008年也验证了一个小的实验性的操作系统内核以展示相关理论和技术上的突破。虽然该内核比seL4小得多，但得益于他们提出的“开放式验证框架理论”的方法学、硬件中断验证技术和汇编程序验证技术，内核的所有代码都得到了验证。

中科大－耶鲁高可信软件联合研究中心成立于2008年10月，以我校计算机学院软件安全实验室的力量为主体，耶鲁大学邵中教授主持的Flint小组给予技术支持和研究合作。双方的合作研究始于2004年，根据研究领域和研究队伍的特点，当初就把目标设定为建设领域内国际一流的研究中心。经历以耶鲁为主合作发表、以我方为主合作发表和我方能够独自发表国际一流水平论文这样几个阶段，联合研究中心已经奠定了坚实的研究基础，形成了以海外引进的冯新宇教授为学术带头人的研究团队。

（计算机学院）