www.8522.com

南大荣誉榜

     

    科研 | 新萄京计算机科学与技术系程序设计语言研究组荣获PLDI 2019杰出论文奖

    发布者:王天悦发布时间:2019-08-05浏览次数:10

           2019年6月22日至26日,第40届程序设计语言设计与实现会议(ACM SIGPLAN Conference on Programming Language Design and Implementation,PLDI 2019)在美国凤凰城举行,新萄京计算机科学与技术系程序设计语言研究组冯新宇教授、梁红瑾副教授及其团队的论文“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ㄍ。

    冯新宇、梁红瑾、蒋瀚如、查君鹏(左起)

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

          (来源:计算机科学与技术系 科学技术处)


    江苏省南京市仙林大道163号新萄京仙林校区行政北楼7楼    版权所有  澳门新萄京赌场

    E-mail:foundation@nju.edu.cn | 电话:+86(25)89686186 | 传真:+86(25)89686186

    请使用IE8以上浏览器或Chrome浏览器以获得最佳效果,最佳分辨率1024*768及以上

    备案号: 苏ICP备10085945-1号

    Baidu
    sogou