2010年5月19日上午，邵中教授在3124教室作了题为“Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software”的学术报告。报告会由计算机科学与技术学院陈意云教授主持，来自07级的计算机学院本科生和其他感兴趣的部分师生参加了报告会。。。。
邵中教授以纽约时报关于“近30年来改变人类生活的最重要的创新”的调查报导引出报告，该调查结果显示这些创新大都完全或部分地与计算机相关，如互联网、PC和膝上计算机、电子邮件、多处理器等。计算机相关的研究成果已广泛应用于并影响着人类生活的各个领域，但是，目前计算机系统资源（如处理器）的利用率不高、众多软件以至整个计算机系统的安全性面临挑战等现状导致人类社会期待着更多计算机研究和技术的创新，也给计算机学科的学生和科研人员带来了众多需要研究解决的问题。邵中教授由衷地指出：“现在学计算机的真是幸运的一代！”这激起了在座听众的热情和兴趣。
纽约时报关于“近30年改变人类生活的最大创新”的报导
随着软件越来越广泛地使用，软件是否可信、如何测量软件的可信性等问题成为计算机科研人员面临的主要挑战之一。邵中教授接着依次从为什么需要携带证明的可信软件、什么是携带证明的可信软件、如何构造可信软件、开放的经过验证的汇编编程框架(OCAP, open framework for certified assembly programming)、验证低级的并发代码等五个方面展开介绍。
邵中教授重点介绍了程序验证，他以嵌入式系统为例，讲解了其巨大的市场价值及研究价值；他结合例子展示了程序验证的过程，并介绍了国际上该领域的最新研究状况。邵中教授认为国内的计算机研究有着巨大的潜力，勉励大家平时要多努力、少浮躁，听众反响热烈。
最后邵中教授向大家介绍了中科大－耶鲁高可信软件联合研究中心的相关工作，他表示大家需要树立“做世界一流科研”的目标，这样才能最大程度地挖掘自己的潜力。联合研究中心于2009年初正式成立，但双方的合作研究已开展5～6年，近年来已在程序语言领域的顶级国际会议PLDI上合作发表了3篇论文。目前，联合中心有3位科大博士生在耶鲁大学做科研，邵中教授表示欢迎更多有志的同学加入联合研究中心。
在将近2个小时的报告会中，邵中教授介绍了程序验证方面的研究内容和研究前景，大家以热烈的掌声向邵中教授的精彩报告表示衷心感谢。报告结束后，同学们踊跃提问，邵中教授均耐心地一一解答。
报告人简介：
邵中教授是我校校友、大师讲席教授。
近年来，邵中教授研究重点集中在开发新的可信软件理论和技术，目标是为开发携带证明的大规模可信系统软件构建一种实用的基础平台。提出了领域专用语言加领域专用逻辑来验证领域专门代码，并连接它们成为完整的可信软件系统的思想和方法。已经开创性地设计了验证操作系统若干部分所需的多种专用逻辑和连接各种证明的开放框架，完成了汇编代码级的垃圾收集和存储分配等库函数、自修改代码的引导程序、非抢占式并发线程等实例程序的验证，最近验证了一个带硬中断和抢占式并发的简单操作系统。
