2010年5月19日上午，邵中教授在3124教室作了題為“Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software”的學術報告。報告會由188滚球网 陳意雲教授主持，來自07級的計算機學院本科生和其他感興趣的部分師生參加了報告會。。。。
邵中教授以紐約時報關於“近30年來改變人類生活的最重要的創新”的調查報導引出報告，該調查結果顯示這些創新大都完全或部分地與計算機相關，如互聯網、PC和膝上計算機、電子郵件、多處理器等。計算機相關的研究成果已廣泛應用於並影響著人類生活的各個領域，但是，目前計算機係統資源（如處理器）的利用率不高、眾多軟件以至整個計算機係統的安全性麵臨挑戰等現狀導致人類社會期待著更多計算機研究和技術的創新，也給計算機學科的學生和科研人員帶來了眾多需要研究解決的問題。邵中教授由衷地指出：“現在學計算機的真是幸運的一代！”這激起了在座聽眾的熱情和興趣。
紐約時報關於“近30年改變人類生活的最大創新”的報導
隨著軟件越來越廣泛地使用，軟件是否可信、如何測量軟件的可信性等問題成為計算機科研人員麵臨的主要挑戰之一。邵中教授接著依次從為什麼需要攜帶證明的可信軟件、什麼是攜帶證明的可信軟件、如何構造可信軟件、開放的經過驗證的彙編編程框架(OCAP, open framework for certified assembly programming)、驗證低級的並發代碼等五個方麵展開介紹。
邵中教授重點介紹了程序驗證，他以嵌入式係統為例，講解了其巨大的市場價值及研究價值；他結合例子展示了程序驗證的過程，並介紹了國際上該領域的最新研究狀況。邵中教授認為國內的計算機研究有著巨大的潛力，勉勵大家平時要多努力、少浮躁，聽眾反響熱烈。
最後邵中教授向大家介紹了中科大－耶魯高可信軟件聯合研究中心的相關工作，他表示大家需要樹立“做世界一流科研”的目標，這樣才能最大程度地挖掘自己的潛力。聯合研究中心於2009年初正式成立，但雙方的合作研究已開展5～6年，近年來已在程序語言領域的頂級國際會議PLDI上合作發表了3篇論文。目前，聯合中心有3位科大博士生在耶魯大學做科研，邵中教授表示歡迎更多有誌的同學加入聯合研究中心。
在將近2個小時的報告會中，邵中教授介紹了程序驗證方麵的研究內容和研究前景，大家以熱烈的掌聲向邵中教授的精彩報告表示衷心感謝。報告結束後，同學們踴躍提問，邵中教授均耐心地一一解答。
報告人簡介：
邵中教授是我校校友、大師講席教授。
近年來，邵中教授研究重點集中在開發新的可信軟件理論和技術，目標是為開發攜帶證明的大規模可信係統軟件構建一種實用的基礎平台。提出了領域專用語言加領域專用邏輯來驗證領域專門代碼，並連接它們成為完整的可信軟件係統的思想和方法。已經開創性地設計了驗證操作係統若幹部分所需的多種專用邏輯和連接各種證明的開放框架，完成了彙編代碼級的垃圾收集和存儲分配等庫函數、自修改代碼的引導程序、非搶占式並發線程等實例程序的驗證，最近驗證了一個帶硬中斷和搶占式並發的簡單操作係統。
