中科大－耶鲁高可信软件联合研究中心成立于2008年10月，以我校计算机学院软件安全实验室的力量为主体，耶鲁大学邵中教授主持的Flint小组给予技术支持和研究合作，目标是建设成为领域内国际一流的研究中心。经过几年的努力，研究中心形成了以海外引进的冯新宇教授为学术带头人的研究团队，在计算机学科国际顶级会议上发表论文多篇，研究水平进入国际一流，中心双方的合作领域也扩大到计算机网络和操作系统等其他研究方向。
今年6月中旬，博士生梁红瑾和导师冯新宇教授在顶级会议PLDI（ACM SIGPLAN Conference on Programming Language Design and Implementation）第34届年会上发表论文“具有不确定线性化点的可线性化的模块化验证”（Modular Verification of Linearizability with Non-Fixed Linearization Points）。PLDI创办于1979年，其论文范围包括语言设计、语言实现、程序分析、编程模型和程序逻辑等围绕编程语言的理论和技术，每年录用30～40篇。此前，中国大陆在PLDI上发表论文数不超过5篇。
梁红瑾和冯新宇的这篇论文提出了一种验证并发算法的线性一致性（linearizability）的程序逻辑，可以用来验证一些公认的验证难度很大的线性化点不固定的算法，具有很强的实用性。审稿人对该文的贡献给予充分肯定，指出“这个证明系统本身是一个重大贡献…，很高兴得知所有这些算法都可以被这项工作所验证”，并指出“该文还有一个新的贡献：用于描述依赖未来的线性化点的尝试–提交（try-commit）指令非常漂亮，值得发表”。与会专家同样给予了很高评价。
2012年1月，梁红瑾和冯新宇就在另一个顶级会议POPL（ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages）第39届年会上发表论文，实现中国大陆零的突破。值得再添一笔的是，他们的第三篇合作论文“基于上下文精化的并发对象进展性刻画”（Characterizing Progress Properties of Concurrent Objects via Contextual Refinements），于今年5月下旬被第24届并发理论国际会议（24th International Conference on Concurrency Theory，简称CONCUR）录用，CONCUR虽非顶级，但也是一流国际会议。
中心双方合作的共同成果也多次在顶级会议上发表。其中最近的一篇是今年6月被顶级会议SIGCOMM第13届年会录用的论文“Maple：使用算法策略简化软件定义网络编程”（Maple: Simplifying SDN Programming Using Algorithmic Policies ）。我校博士生王俊昌（导师华蓓教授）是该论文的第二作者（按姓名字母序），耶鲁方的合作指导老师是杨阳（Richard Yang）教授。
软件定义网络是现代网络的一个重大观念突破。它采用一种控制面与网络物理拓扑分离的新型网络架构。因此用户可以通过编写运行在集中式控制器上的程序来控制自己的网络流，从而极大地方便网络创新。Maple的贡献是它使得软件定义网络的编写从低级“汇编语言”时代前进到了“高级语言”时代。审稿人对Maple的贡献给予充分肯定：“难以想象Maple这样的做法竟然可行 (Too good to know that it can be true) ”。该论文被提名为最佳论文奖。
目前，联合研究中心除了继续做好基础研究外，中心团队正在学校和计算机学院的支持下，有计划地开展与企业的合作，引导有理论基础并擅长研发的团队成员进行高可信软件开发工具的原型系统研发。
（中科大－耶鲁高可信软件联合研究中心）
