南京大学计算机科学系杨浩然,科研 | 南京大学计算机科学与技术系程序设计语言研究组荣获PLDI 2019杰出论文奖...

本文主要是介绍南京大学计算机科学系杨浩然,科研 | 南京大学计算机科学与技术系程序设计语言研究组荣获PLDI 2019杰出论文奖...,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

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)。

323ada69f4e040aacf40ecef7e0f94c9.png

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

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

f113da8e4cf89d04693443f43f315446.png

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

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

这篇关于南京大学计算机科学系杨浩然,科研 | 南京大学计算机科学与技术系程序设计语言研究组荣获PLDI 2019杰出论文奖...的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!


原文地址:https://blog.csdn.net/weixin_28996271/article/details/117991525
本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.chinasem.cn/article/336583

相关文章

深入理解Go语言中二维切片的使用

《深入理解Go语言中二维切片的使用》本文深入讲解了Go语言中二维切片的概念与应用,用于表示矩阵、表格等二维数据结构,文中通过示例代码介绍的非常详细,需要的朋友们下面随着小编来一起学习学习吧... 目录引言二维切片的基本概念定义创建二维切片二维切片的操作访问元素修改元素遍历二维切片二维切片的动态调整追加行动态

Go语言中make和new的区别及说明

《Go语言中make和new的区别及说明》:本文主要介绍Go语言中make和new的区别及说明,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录1 概述2 new 函数2.1 功能2.2 语法2.3 初始化案例3 make 函数3.1 功能3.2 语法3.3 初始化

Go语言中nil判断的注意事项(最新推荐)

《Go语言中nil判断的注意事项(最新推荐)》本文给大家介绍Go语言中nil判断的注意事项,本文给大家介绍的非常详细,对大家的学习或工作具有一定的参考借鉴价值,需要的朋友参考下吧... 目录1.接口变量的特殊行为2.nil的合法类型3.nil值的实用行为4.自定义类型与nil5.反射判断nil6.函数返回的

Go语言数据库编程GORM 的基本使用详解

《Go语言数据库编程GORM的基本使用详解》GORM是Go语言流行的ORM框架,封装database/sql,支持自动迁移、关联、事务等,提供CRUD、条件查询、钩子函数、日志等功能,简化数据库操作... 目录一、安装与初始化1. 安装 GORM 及数据库驱动2. 建立数据库连接二、定义模型结构体三、自动迁

Go语言代码格式化的技巧分享

《Go语言代码格式化的技巧分享》在Go语言的开发过程中,代码格式化是一个看似细微却至关重要的环节,良好的代码格式化不仅能提升代码的可读性,还能促进团队协作,减少因代码风格差异引发的问题,Go在代码格式... 目录一、Go 语言代码格式化的重要性二、Go 语言代码格式化工具:gofmt 与 go fmt(一)

Qt如何实现文本编辑器光标高亮技术

《Qt如何实现文本编辑器光标高亮技术》这篇文章主要为大家详细介绍了Qt如何实现文本编辑器光标高亮技术,文中的示例代码讲解详细,具有一定的借鉴价值,有需要的小伙伴可以了解下... 目录实现代码函数作用概述代码详解 + 注释使用 QTextEdit 的高亮技术(重点)总结用到的关键技术点应用场景举例示例优化建议

Go语言中泄漏缓冲区的问题解决

《Go语言中泄漏缓冲区的问题解决》缓冲区是一种常见的数据结构,常被用于在不同的并发单元之间传递数据,然而,若缓冲区使用不当,就可能引发泄漏缓冲区问题,本文就来介绍一下问题的解决,感兴趣的可以了解一下... 目录引言泄漏缓冲区的基本概念代码示例:泄漏缓冲区的产生项目场景:Web 服务器中的请求缓冲场景描述代码

Go语言如何判断两张图片的相似度

《Go语言如何判断两张图片的相似度》这篇文章主要为大家详细介绍了Go语言如何中实现判断两张图片的相似度的两种方法,文中的示例代码讲解详细,感兴趣的小伙伴可以跟随小编一起学习一下... 在介绍技术细节前,我们先来看看图片对比在哪些场景下可以用得到:图片去重:自动删除重复图片,为存储空间"瘦身"。想象你是一个

Go语言中Recover机制的使用

《Go语言中Recover机制的使用》Go语言的recover机制通过defer函数捕获panic,实现异常恢复与程序稳定性,具有一定的参考价值,感兴趣的可以了解一下... 目录引言Recover 的基本概念基本代码示例简单的 Recover 示例嵌套函数中的 Recover项目场景中的应用Web 服务器中

Java中的登录技术保姆级详细教程

《Java中的登录技术保姆级详细教程》:本文主要介绍Java中登录技术保姆级详细教程的相关资料,在Java中我们可以使用各种技术和框架来实现这些功能,文中通过代码介绍的非常详细,需要的朋友可以参考... 目录1.登录思路2.登录标记1.会话技术2.会话跟踪1.Cookie技术2.Session技术3.令牌技