邵中

1983年，進入中國科學技術大學少年班。 ^[3] 

1988年，畢業於中國科學技術大學計算機系，獲計算機科學學士學位。 ^[3] 

1994年，畢業於普林斯頓大學，獲計算機科學博士學位。 ^[3] 

1994年起，在耶魯大學計算機系任教。 ^[3] 

2003年，任耶魯大學計算機系教授。 ^[3] 

兼任中國科大客座教授、清華大學姚期智小組講席教授, 以及中華全國青聯第十屆委員會常務委員。 ^[4] 

成為中國科大－耶魯大學可信軟件聯合研究中心主任。 ^[5] 

任ACM SIGPLAN 執行委員會委員，並擔任程序設計語言領域多種國際會議和期刊的評審委員會委員和編委。 ^[5] 

2016年11月，其領導的耶魯大學研究團隊推出了 CertiKOS，這是世界上第一個在多核處理器上運行並可防禦網絡攻擊的操作系統。 ^[6] 

2018年12月，任命為 Thomas L. Kempner 計算機科學教授，主要研究編程語言、編譯器、形式化驗證和操作系統。 ^[7] 

2018年，邵中教授與哥倫比亞大學計算機系顧榮輝教授共同成立CertiK。 ^[8] 

近年來，研究重點集中在開發新的程序驗證理論和技術，目標是為開發經過驗證的大規模系統軟件構建一種實用的基礎平台。提出了領域專用語言加領域專用邏輯來驗證領域專門代碼並連接它們成為完整的經過驗證的軟件系統的思想和方法。已經開創性地設計了驗證操作系統若干部分所需的多種專用邏輯和連接各種證明的開放框架，完成了彙編代碼級的垃圾收集和存儲分配等庫函數、自修改代碼的引導程序、非搶佔式併發線程等實例程序的驗證，最近驗證了一個帶硬中斷和搶佔式併發的簡單操作系統。 ^[1] 

1．2009年起，擔任ACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL)指導委員會主席

2．擔任第36屆ACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages(POPL’09)大會主席

3．擔任第5屆AsianSymposiumonProgrammingLanguagesandSystems(APLAS’07)大會程序主席

4．各種國際學術會議和學術討論會的程序委員會委員，包括：SSV’09，POPL’08，SSV’08，TASE’07，TFP’07，CC’07，APLAS’06，ATVA’06，TFP’06，POPL’05，ICFP’03，APLAS’03，PLDI’99，TIC’98，POPL’965．各種學術雜誌的編委，包括：JournalofFunctionalProgramming(2001–)，JournalofComputingScienceandEngineering(2007–)，JournalofComputerScienceandTechnology(2006–)6.2001–2005，ACMSIGPLAN執行委員會學術委員（MembersatLarge） ^[1] 

高可信軟件、程序設計語言及編譯、操作系統 ^[1] 

1．1988年中國科學技術大學郭沫若獎學金

2．1995－1998年美國國家科學基金青年學者獎 ^[1] 

3. 2015年，獲得美國國家科學基金會計算探險獎，深度規範科學。 ^[9] 

4. 2017年，成為康涅狄格州科學與工程院院士 ^[10] 

5. 2022年，任ACM SIGPLAN年度編程語言會議外部評審委員會成員 （PLDI 2022） ^[11] 

2017年7月，邵中受邀於CCF-GAIR 2017大會發表主題演講，闡述了“反黑客攻擊”操作系統CertiKOS背後的理念，並表示操作系統發展拐點已到。 ^[12] 

2018年3月，邵中在《雷鋒網》的報道中表示，一旦所有的區塊鏈的代碼在上鍊前全部被形式化的數學證明驗證後，開發者和用户們就無須再為區塊鏈上的系統遭受黑客攻擊而擔心，區塊鏈的安全性問題能夠真正得到解決。 ^[13]