中科大研究论文被POPL录用 －－为大陆研究机构首篇被录用论

rock.li

日前，中科大－耶鲁高可信软件联合研究中心梁红瑾、冯新宇和付明的论文“一种用于验证并发程序变换的基于依赖-保证的模拟关系”（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）中，成功地解决了对验证提供模块化支持的难题，并将这种方法应用于编译优化、并发数据结构的实现和并发垃圾收集等算法的正确性验证。审稿人对论文的贡献给予了充分肯定，他们分别指出：“我感到这篇文章很吸引人。结合模拟关系与依赖-保证推理的想法看起来很不错，而且我在别处都没有见过……这项工作能提供一种漂亮的统一理论，用于验证并发程序变换。”“并发系统的精化问题的研究非常具有挑战性，这篇文章则向这个领域迈出了很好的一步。”“一个能够同时支持运行时系统验证和编译器验证的逻辑将非常有用。这篇文章展示了这样一个逻辑，并且看起来是一种非常普适的、自然的方法。”

qfg666

祝贺一下