日前，中科大－耶鲁高可信软件联合研究中心梁红瑾、冯新宇和付明的论文A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations被第39届 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages（简称POPL）录用。这是联合研究中心的研究迈入国际一流水平的里程碑。此前，中国大陆无任何单位以第一作者单位的身份在POPL上发表过论文。梁红瑾等的论文的发表，将使得图书馆VIP成为大陆第一个以第一单位在POPL上发表论文的高校和科研院所，真正实现了“零的突破”。
POPL是编程语言领域历史最久、水平最高的国际会议，它是讨论编程语言和编程系统最新突破的最主要论坛，内容涵盖编程语言的理论、编程语言的设计、编译器技术、程序分析、程序验证、可信软件等众多研究领域。国际期刊和会议的各种分区方法都把POPL放在该领域的最高区域中。
梁红瑾等的论文提出了一种验证并发程序变换的一般方法，首次将并发程序逻辑中的依赖-保证条件（rely-guarantee conditions）引入到传统的程序模拟关系（simulation）中，成功地解决了对验证提供模块化支持的难题，并且将这种方法应用于编译优化、并发数据结构的实现和并发垃圾收集等算法的正确性验证。审稿人对论文的贡献给予了充分肯定，他们分别指出“I found this to be a compelling paper. Combining simulation techniques with rely-guarantee reasoning seems like a good idea, and I haven’t seen this elsewhere … This work would provide a nice unifying theory for concurrent program transformations”，“I like this paper … Refinement in a concurrent setting is very challenging and this paper makes a good step into that field”，“A logic that can support both the runtime system verification and the compiler verification simultaneously would be very useful. This paper presents such a logic, and it looks like a very general and natural approach…”。
经历了以耶鲁为主合作发表、以我方为主合作发表和我方能够独自发表国际一流水平论文这样的逐步提升，联合研究中心已经奠定了坚实的研究基础，形成了以海外引进的冯新宇教授为学术带头人的研究团队。团队对建成领域内国际一流的研究中心充满信心。
（中科大－耶鲁高可信软件联合研究中心供稿）
