中科大188滚球网 於2010年暑期首次開辦三門小學期課程，其中“可信軟件的前沿理論和技術”課程由中科大-耶魯高可信軟件聯合研究中心邵中老師（耶魯大學教授，我校“大師講席”教授）領銜主講。該課程於7月19日開始，至7月25日結束，課程由每天上午的理論教學和下午的上機實踐組成。前來參加課程的同學主要是來自於計算機學院各年級的本科生、研究生，同時還有電子工程學院和其他院係感興趣的師生。
課程理論教學圍繞高可信軟件所用到的程序驗證理論和技術等展開，包括函數式語言和演算、程序驗證的邏輯基礎、並行程序的驗證、自動定理證明、出具證明編譯器等專題。理論教學由聯合研究中心的邵中教授、陳意雲教授、張昱副教授、郭宇博士後和李兆鵬博士後主講。各位老師風趣、嚴謹、細致的教學風格給聽課師生留下了深刻印象。下圖為同學們在專注地聽邵中教授講課。
課程上機實踐主要包括使用函數式語言OCAML進行函數式編程、使用定理證明工具Coq驗證函數式程序和命令式程序，使用ESC/Java2和聯合研究中心自行研發的出具證明編譯器CCOMP等工具進行程序和規範編寫、調試。聯合研究中心精心準備和設計了實驗案例，每次上機實踐均安排多名博士後和博士生進行悉心指導，使同學們通過上機實踐對程序分析和驗證的相關理論和技術有了更深刻的理解。圖為同學們在助教的輔導下進行上機實踐。
在課程開設前，很多同學對程序可靠性的認識尚都停留在軟件測試的層麵。通過課程學習，很多同學都對高可信軟件能夠在某種程度上達到數學意義上的無bug感到神奇。有同學這樣說：“從來沒想過軟件有沒有bug也可以驗證”“這個領域太有趣了”等等。課程結束後多位同學主動與授課老師交流，表示希望能繼續在該領域進行深入學習。
整個課程總結了高可信軟件研究領域中的國際前沿理論和技術，也介紹了中科大-耶魯高可信軟件聯合研究中心的相關研究成果，使同學們了解該領域的理論技術，激發了對該領域的興趣和從事科研工作的熱情。
聯合研究中心暑期課程主頁（http://kyhcs.ustcsz.edu.cn/summer-school）提供本課程的全部授課資料。
