邵中，全球領先的Web3.0安全機構CertiK的聯合創始人，同時也是耶魯大學計算機系教授。他同時還擔任中國科大－耶魯高可信軟體聯合研究中心的主任、中國科大的大師講席教授。
邵中教授是電腦程式語言設計和實現領域的國際專家，他是學術界和工業界科研項目中廣泛使用的SML/NJ函式式程式語言的編譯器的主要設計和實現者之一，研究成果包括基於後續傳遞風格的編譯方法等多項成果。
基本介紹
- 中文名：邵中
- 出生日期：1968年8月
- 主要成就：美國國家科學基金青年學者獎
- 職稱：教授
個人履歷,主要學術任職,主要研究方向,榮譽頭銜,新聞報導,
個人履歷
1983年，進入中國科學技術大學少年班。
1988年，畢業於中國科學技術大學計算機系，獲計算機科學學士學位。
1994年，畢業於普林斯頓大學，獲計算機科學博士學位。
1994年起，在耶魯大學計算機系任教。
2003年，任耶魯大學計算機系教授。
兼任中國科大客座教授、清華大學姚期智小組講席教授, 以及中華全國青聯第十屆委員會常務委員。
成為中國科大－耶魯大學可信軟體聯合研究中心主任。
任ACM SIGPLAN 執行委員會委員，並擔任程式設計語言領域多種國際會議和期刊的評審委員會委員和編委。
2016年11月，其領導的耶魯大學研究團隊推出了 CertiKOS，這是世界上第一個在多核處理器上運行並可防禦網路攻擊的作業系統。
2018年12月，任命為 Thomas L. Kempner 計算機科學教授，主要研究程式語言、編譯器、形式化驗證和作業系統。
2018年，邵中教授與哥倫比亞大學計算機系顧榮輝教授共同成立CertiK。
近年來，研究重點集中在開發新的程式驗證理論和技術，目標是為開發經過驗證的大規模系統軟體構建一種實用的基礎平台。提出了領域專用語言加領域專用邏輯來驗證領域專門代碼並連線它們成為完整的經過驗證的軟體系統的思想和方法。已經開創性地設計了驗證作業系統若干部分所需的多種專用邏輯和連線各種證明的開放框架，完成了彙編代碼級的垃圾收集和存儲分配等庫函式、自修改代碼的引導程式、非搶占式並發執行緒等實例程式的驗證，最近驗證了一個帶硬中斷和搶占式並發的簡單作業系統。
主要學術任職
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）
主要研究方向
高可信軟體、程式設計語言及編譯、作業系統
榮譽頭銜
2．1995－1998年美國國家科學基金青年學者獎
3. 2015年，獲得美國國家科學基金會計算探險獎，深度規範科學。
4. 2017年，成為康乃狄克州科學與工程院院士
5. 2022年，任ACM SIGPLAN年度程式語言會議外部評審委員會成員 （PLDI 2022）
新聞報導
2017年7月，邵中受邀於CCF-GAIR 2017大會發表主題演講，闡述了“反黑客攻擊”作業系統CertiKOS背後的理念，並表示作業系統發展拐點已到。
2018年3月，邵中在《雷鋒網》的報導中表示，一旦所有的區塊鏈的代碼在上鏈前全部被形式化的數學證明驗證後，開發者和用戶們就無須再為區塊鏈上的系統遭受黑客攻擊而擔心，區塊鏈的安全性問題能夠真正得到解決。
