中科大-耶鲁 高可信软件联合研究中心

       高可信软件的研究着眼于应用前沿的技术和工具, 显著提高当今计算机软件的可靠性. 高可信软件的研究需要深入的专业知识和对大量计算机学科相关领域的了解, 包括形式化方法, 程序语言, 编译器, 操作系统, 信息安全, 辅助定理证明器, 软件工程, 体系结构和嵌入式操作系统.
       2008年10月, 中国科学技术大学校长侯建国和耶鲁大学校长Richard Levin签署了关于成立科大耶鲁高可信软件联合研究中心的备忘录. 新成立的中心联合了两所大学的人力和物力资源. 中心的长远目标是支持各个独立的研究小组共享资源和专业技能, 开展多领域的研究. 中国科学技术大学和耶鲁大学将通过中心使得两所大学间的高可信软件后研究小组的直接合作更加紧密. 同时, 双方也会开展定期的交换生和访问学者的交流.
        联合中心旨在研究高可信软件和形式化方法的各个领域. 当前的研究课题包括形式化验证系统软件, 出具证明的编译器, 并行和多核的软件以及自动定理证明系统等. 联合中心在探索结合形式化程序验证和领域专用语言和逻辑进行软件开发的新方法, 以及为大规模的以工业应用为目标的验证的系统软件进行基础研究. 这些研究的成功会显著推进当今可靠软件的开发.