中科大8797威尼斯老品牌于2010年暑期首次开办三门小学期课程，其中“可信软件的前沿理论和技术”课程由中科大-耶鲁高可信软件联合研究中心邵中老师（耶鲁大学教授，我校“大师讲席”教授）领衔主讲。该课程于7月19日开始，至7月25日结束，课程由每天上午的理论教学和下午的上机实践组成。前来参加课程的同学主要是来自于计算机学院各年级的本科生、研究生，同时还有电子工程学院和其他院系感兴趣的师生。
课程理论教学围绕高可信软件所用到的程序验证理论和技术等展开，包括函数式语言和演算、程序验证的逻辑基础、并行程序的验证、自动定理证明、出具证明编译器等专题。理论教学由联合研究中心的邵中教授、陈意云教授、张昱副教授、郭宇博士后和李兆鹏博士后主讲。各位老师风趣、严谨、细致的教学风格给听课师生留下了深刻印象。下图为同学们在专注地听邵中教授讲课。
课程上机实践主要包括使用函数式语言OCAML进行函数式编程、使用定理证明工具Coq验证函数式程序和命令式程序，使用ESC/Java2和联合研究中心自行研发的出具证明编译器CCOMP等工具进行程序和规范编写、调试。联合研究中心精心准备和设计了实验案例，每次上机实践均安排多名博士后和博士生进行悉心指导，使同学们通过上机实践对程序分析和验证的相关理论和技术有了更深刻的理解。图为同学们在助教的辅导下进行上机实践。
在课程开设前，很多同学对程序可靠性的认识尚都停留在软件测试的层面。通过课程学习，很多同学都对高可信软件能够在某种程度上达到数学意义上的无bug感到神奇。有同学这样说：“从来没想过软件有没有bug也可以验证”“这个领域太有趣了”等等。课程结束后多位同学主动与授课老师交流，表示希望能继续在该领域进行深入学习。
整个课程总结了高可信软件研究领域中的国际前沿理论和技术，也介绍了中科大-耶鲁高可信软件联合研究中心的相关研究成果，使同学们了解该领域的理论技术，激发了对该领域的兴趣和从事科研工作的热情。
联合研究中心暑期课程主页（http://kyhcs.ustcsz.edu.cn/summer-school）提供本课程的全部授课资料。
