個(gè)人簡介
近年來，研究重點(diǎn)集中在開發(fā)新的程序驗(yàn)證理論和技術(shù)，目標(biāo)是為開發(fā)經(jīng)過驗(yàn)證的大規(guī)模系統(tǒng)軟件構(gòu)建一種實(shí)用的基礎(chǔ)平臺(tái)。提出了領(lǐng)域?qū)Ｓ谜Z言加領(lǐng)域?qū)Ｓ眠壿媮眚?yàn)證領(lǐng)域?qū)ｉT代碼并連接它們成為完整的經(jīng)過驗(yàn)證的軟件系統(tǒng)的思想和方法。已經(jīng)開創(chuàng)性地設(shè)計(jì)了驗(yàn)證操作系統(tǒng)若干部分所需的多種專用邏輯和連接各種證明的開放框架，完成了匯編代碼級(jí)的垃圾收集和存儲(chǔ)分配等庫函數(shù)、自修改代碼的引導(dǎo)程序、非搶占式并發(fā)線程等實(shí)例程序的驗(yàn)證，最近驗(yàn)證了一個(gè)帶硬中斷和搶占式并發(fā)的簡單操作系統(tǒng)。
主要學(xué)術(shù)任職
1．2009年起，擔(dān)任A CMSIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL)指導(dǎo)委員會(huì)主席
2．擔(dān)任第36屆A CMSIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPLu201909)大會(huì)主席
3．擔(dān)任第5屆Asian Symposium on Programming Language sand Systems(APLASu201907)大會(huì)程序主席
4．各種國際學(xué)術(shù)會(huì)議和學(xué)術(shù)討論會(huì)的程序委員會(huì)委員，包括：SSVu201909，POPLu201908，SSVu201908，TASEu201907，TFPu201907，CCu201907，APLASu201906，ATVAu201906，TFPu201906，POPLu201905，ICFPu201903，APLASu201903，PLDIu201999，TICu201998，POPLu2019965．各種學(xué)術(shù)雜志的編委，包括：Journal of unctional Programming(2001u2013)，Journal of Computing Science and Engineering(2007u2013)，Journal of Computer Science and Technology(2006u2013)6.2001u20132005，ACMSIGPLAN執(zhí)行委員會(huì)學(xué)術(shù)委員（Membersat Large）
主要研究方向
高可信軟件、程序設(shè)計(jì)語言及編譯、操作系統(tǒng)
獲獎(jiǎng)情況
1．1988年中國科學(xué)技術(shù)大學(xué)郭沫若獎(jiǎng)學(xué)金
2．1995－1998年美國國家科學(xué)基金青年學(xué)者獎(jiǎng)
