2019年6月22日至26日，第40届程序设计语言设计与实现会议（ACM SIGPLAN Conference on Programming Language Design and Implementation，PLDI 2019）在美国凤凰城举行，37000cm威尼斯计算机科学与技术系程序设计语言研究组冯新宇教授、梁红瑾副教授及其团队的论文“Towards Certified Separate Compilation for Concurrent Programs”荣获本次会议的杰出论文奖（Distinguished Paper Award）。

该获奖论文关注并发程序的分离编译的验证问题。编译器是一种重要的基础系统软件，它将程序员用高级语言编写的程序（即“源程序”）翻译成机器可执行的二进制代码（称为“目标码”）。然而，现实世界中绝大多数编译器（如GCC、LLVM、CIL、TCC、Open64等）都存在“误编译”的问题，会将正确的源程序编译成有缺陷的目标码，从而导致程序在运行的时候出错或崩溃。编译器的验证能确保编译器的正确性，从而保证编译过程不会引入错误。该论文提出了一种通用的理论框架，能够将串行程序编译的正确性验证工作复用于并发程序分离编译的验证。利用这一框架，论文作者还开发了并发C程序的分离编译器CASCompCert并验证了其正确性。该论文附带的编译器工具及相关证明还通过了本次会议的工具评估（Artifact Evaluation）委员会的评审，获得了ACM工具评估徽章。

PLDI是程序设计语言领域的顶级会议之一，创办于1979年，其论文范围包括语言设计、语言实现、程序分析、编程模型和程序逻辑等围绕程序设计语言的理论和技术。本次会议从283篇投稿论文中，收录论文76篇，其中6篇论文获Distinguished Paper Award。计算机系程序设计语言研究组冯新宇教授为此次获奖论文的通讯作者，梁红瑾副教授为共同第一作者，论文的其他作者为其指导的中国科学技术大学的研究生蒋瀚如、肖思扬和查君鹏。此次获奖为PLDI召开40年来中国大陆科研院所为第一单位的论文首次获得PLDI Distinguished Paper Award。

冯新宇、梁红瑾、蒋瀚如、查君鹏（左起）

37000cm威尼斯计算机科学与技术系程序设计语言研究组主要从事程序设计语言理论和形式化程序验证方面的研究，此前关于并发程序验证和操作系统内核验证的多项成果发表在POPL、PLDI、LICS、CAV和ACM TOPLAS等CCF A类国际会议和期刊上。此项工作部分获得国家自然科学基金和华为创新研究计划（HIRP）项目的支持。

（计算机科学与技术系 科学技术处）