中国科大在并发程序精化验证领域取得突破

http://www.cas.ac.cn/ky/kyjz/201312/t20131226_4005994.shtml
近日，中国科学技术大学计算机科学与技术学院博士生梁红瑾和导师冯新宇教授等人在并发程序精化验证领域取得突破，提出了一种基于依赖－保证的模拟技术（简称RGSim），用以支持并发程序间的精化关系的模块化验证。研究成果已被计算机学科国际期刊TOPLAS正式录用。

　　程序精化验证旨在证明不同计算机程序行为之间的包含关系，是形式化程序验证领域的经典理论问题，同时具有广阔的应用前景。然而，在多处理器下运行的并发程序之间的精化关系验证始终是该领域的一个难题。传统的验证技术要么在封闭环境下进行验证，因而需要知道完整程序的信息，无法支持局部的模块化验证；要么支持开放环境，但对环境的行为没有任何约束，因而验证过程无法利用针对特定环境的知识，难以用来解决实际问题。

　　梁红瑾等人提出了一种RGSim技术，用以支持并发程序间的精化关系的模块化验证。RGSim支持开放环境下的验证，但同时允许把关于特定环境的知识体现在当前被验证线程的依赖关系中，因而可以根据特定应用下的特定环境来定制程序间的模拟关系，进而推导出精化关系。RGSim技术一方面支持并发程序精化的模块化验证，一方面又具备较强的通用性和应用价值，能够应用于并发程序原子性验证、并发编译优化算法验证以及并发垃圾收集算法验证等。

　　TOPLAS创刊于1979年，平均每年刊出论文约25篇。到目前为止，中国大陆仅中科院软件研究所作为第一单位于1993年在该刊上发表1篇论文。

　　此前，梁红瑾等曾于2012年在POPL第39届年会上发表论文1篇，实现了中国大陆科研院所在POPL发表论文的零的突破。另外，还在今年6月份的PLDI第34届年会上发表论文1篇，这是中国大陆在PLDI上发表的第6篇论文。这两篇论文和此次录用的TOPLAS论文对并发程序精化验证从理论和应用两个方面进行了逐步深入的系统探讨，体现了针对该问题研究的最新进展。

　　梁红瑾2009年本科毕业于中国科大少年班，推免进计算机学院，加入中科大－耶鲁高可信软件联合研究中心，2011年开始攻读博士学位。 http://www.cas.ac.cn/ky/kyjz/201312/t20131226_4005994.shtml
近日，中国科学技术大学计算机科学与技术学院博士生梁红瑾和导师冯新宇教授等人在并发程序精化验证领域取得突破，提出了一种基于依赖－保证的模拟技术（简称RGSim），用以支持并发程序间的精化关系的模块化验证。研究成果已被计算机学科国际期刊TOPLAS正式录用。

　　程序精化验证旨在证明不同计算机程序行为之间的包含关系，是形式化程序验证领域的经典理论问题，同时具有广阔的应用前景。然而，在多处理器下运行的并发程序之间的精化关系验证始终是该领域的一个难题。传统的验证技术要么在封闭环境下进行验证，因而需要知道完整程序的信息，无法支持局部的模块化验证；要么支持开放环境，但对环境的行为没有任何约束，因而验证过程无法利用针对特定环境的知识，难以用来解决实际问题。

　　梁红瑾等人提出了一种RGSim技术，用以支持并发程序间的精化关系的模块化验证。RGSim支持开放环境下的验证，但同时允许把关于特定环境的知识体现在当前被验证线程的依赖关系中，因而可以根据特定应用下的特定环境来定制程序间的模拟关系，进而推导出精化关系。RGSim技术一方面支持并发程序精化的模块化验证，一方面又具备较强的通用性和应用价值，能够应用于并发程序原子性验证、并发编译优化算法验证以及并发垃圾收集算法验证等。

　　TOPLAS创刊于1979年，平均每年刊出论文约25篇。到目前为止，中国大陆仅中科院软件研究所作为第一单位于1993年在该刊上发表1篇论文。

　　此前，梁红瑾等曾于2012年在POPL第39届年会上发表论文1篇，实现了中国大陆科研院所在POPL发表论文的零的突破。另外，还在今年6月份的PLDI第34届年会上发表论文1篇，这是中国大陆在PLDI上发表的第6篇论文。这两篇论文和此次录用的TOPLAS论文对并发程序精化验证从理论和应用两个方面进行了逐步深入的系统探讨，体现了针对该问题研究的最新进展。

　　梁红瑾2009年本科毕业于中国科大少年班，推免进计算机学院，加入中科大－耶鲁高可信软件联合研究中心，2011年开始攻读博士学位。