扎實打根基 創(chuàng)新展宏圖
——記上海交通大學(xué)電子信息與電氣工程學(xué)院特別副研究員符鴻飛

◎ 文/曹 莉

他對科研的態(tài)度是嚴(yán)謹(jǐn)治學(xué)、打牢根基。他創(chuàng)新的 “形式化驗證”是一種從理論上進(jìn)行測試的全新方法，被形象地稱作為 “窮盡式數(shù)學(xué)技術(shù)”，其原理是利用數(shù)學(xué)和邏輯的方法來證明計算機(jī)系統(tǒng)的正確性。

他長期致力于理論計算機(jī)科學(xué)中的形式化驗證領(lǐng)域研究，在獲得一系列原創(chuàng)性理論成果的同時，緊密結(jié)合工業(yè)界生產(chǎn)實際，致力于把理論成果成功地轉(zhuǎn)化為工業(yè)實踐，并取得了豐碩的成果。

他的學(xué)術(shù)成就豐富，在理論計算機(jī)科學(xué)、形式化方法國際著名學(xué)術(shù)會議及期刊上以主要貢獻(xiàn)者身份發(fā)表論文14篇，為ICALP、VMCAI、FOSSACS、Information and Computation、Information Processing Letter等審稿30余篇，參與國家自然科學(xué)基金重點項目1項，獲得國家自然科學(xué)青年基金資助1項，曾獲HSCC 2013年度最佳學(xué)生論文獎以及科學(xué)中國人2017年度人物。

他就是上海交通大學(xué)電子信息與電氣工程學(xué)院特別副研究員符鴻飛。

熱愛專業(yè)領(lǐng)域,邁向縱深地帶

作為學(xué)者，符鴻飛是個愛學(xué)習(xí)愛鉆研的人。任何一門學(xué)科，任何一個專業(yè)要想深入學(xué)習(xí)了解，真正掌握其中的奧秘，就必須有無比熱愛的胸懷和敢于向縱深地帶不斷探索前進(jìn)的精神。符鴻飛的身上具有這種科研的精神特質(zhì)，這種特質(zhì)來自于他對專業(yè)領(lǐng)域不斷學(xué)習(xí)、研究和攻關(guān)。

當(dāng)他回憶起自己的成長之路時，心情一如陽光那般燦爛。2003年，他考入上海交通大學(xué)計算機(jī)科學(xué)與技術(shù)專業(yè)。他說：“當(dāng)時之所以會選擇計算機(jī)專業(yè)是因為想探索與數(shù)學(xué)有一定聯(lián)系的計算機(jī)問題。”他清楚地記得自己在讀本科期間對如何保證程序編寫的正確性產(chǎn)生過困惑，因此在寫完程序后往往會反復(fù)讀幾遍程序，確保程序不會出錯。而這種寫程序的方法與通常測試檢驗程序的方法相比速度比較慢，但通過這種寫程序的方法又有缺陷較少的優(yōu)點，使后期調(diào)試過程變得相應(yīng)較短。他興奮于自己的研究發(fā)現(xiàn)，加速了他向形式化驗證這個縱深領(lǐng)域邁進(jìn)的步伐。

符鴻飛真正對利用數(shù)學(xué)方法證明系統(tǒng)正確性的形式化驗證領(lǐng)域產(chǎn)生濃厚興趣的是在他碩士研究生階段。攻讀研究生期間，他選擇了上海交通大學(xué)傅育熙教授作為自己的導(dǎo)師。傅教授的研究方向是理論計算機(jī)科學(xué)中的進(jìn)程理論。正是在傅教授的指導(dǎo)下，符鴻飛對一些無窮狀態(tài)進(jìn)程模型的可判定性和計算復(fù)雜性進(jìn)行了全面系統(tǒng)的研究，并在互模擬判定以及模型檢測算法方面作出了理論上的貢獻(xiàn)。

學(xué)習(xí)最大的樂趣就是不斷有新發(fā)現(xiàn)新方向，從而不斷挺進(jìn)縱深研究地帶。為把形式化驗證學(xué)透搞通，形成形式化驗證的一套方法體系，他通過國家公派留學(xué)找到了該領(lǐng)域著名學(xué)者Joost-Pieter Katoen教授，赴德國亞琛工業(yè)大學(xué)攻讀與形式化驗證相關(guān)的博士。期間，他重點研究了概率系統(tǒng)形式化驗證，獨自給出了諸多相關(guān)理論問題的基礎(chǔ)算法和計算復(fù)雜性，并逐漸由純理論轉(zhuǎn)向理論與應(yīng)用相結(jié)合。在花費4年時間攻讀完博士并拿到學(xué)位后，符鴻飛又踏上了博士后研究的征程，與奧地利科學(xué)技術(shù)研究院（IST Austria） 的Krishnendu Chatterjee教授合作研究概率程序的形式化驗證，并發(fā)表了多篇關(guān)于基礎(chǔ)理論的結(jié)果。

隨著嚴(yán)謹(jǐn)求學(xué)的不斷深入，他逐漸形成了一個觀點，那就是程序驗證（即針對程序的形式化驗證）領(lǐng)域是理論和應(yīng)用相結(jié)合的一個范例，在理論上可以開拓新的形式化驗證領(lǐng)域，在應(yīng)用上也可以和無運行時錯誤保證、無安全漏洞等重要的實際應(yīng)用相結(jié)合。而程序驗證方向也同他本科時遇到的如何保證寫對程序這個問題高度一致。這令他甚感欣慰。

2017年，他帶著回報祖國、感恩母校的情懷從國外歸來，一如自己所愿，成為上海交通大學(xué)電子信息與電氣工程學(xué)院集體的一分子，并任特別副研究員，這讓他倍感榮幸與快樂。在此，他開始新的科研跋涉之旅，但他不問艱辛只管耕耘。

創(chuàng)新關(guān)鍵成果,推進(jìn)科學(xué)發(fā)展

計算機(jī)系統(tǒng)的正確性在安全或任務(wù)關(guān)鍵系統(tǒng)中是一個核心課題。由于潛在的漏洞可能導(dǎo)致重大的人生或財產(chǎn)損失，如何保證關(guān)鍵系統(tǒng)不出現(xiàn)重大漏洞是一個重要的問題。

近年來，隨著計算機(jī)系統(tǒng)越來越復(fù)雜，通過傳統(tǒng)測試方法越來越難以覆蓋足夠多的系統(tǒng)執(zhí)行路徑。因此，致力于理論計算機(jī)科學(xué)中的形式化驗證領(lǐng)域研究的符鴻飛利用數(shù)學(xué)和邏輯的方法來證明計算機(jī)系統(tǒng)研究領(lǐng)域的正確性，在理論背景和實際應(yīng)用成果上可知，形式化驗證為全覆蓋的、自動化的系統(tǒng)正確性證明提供了一個行之有效的方法。作為理論計算機(jī)科學(xué)的一個重要分支，形式化驗證為關(guān)鍵系統(tǒng)組件正確性的自動化推理和證明提供了堅實的基礎(chǔ)，因此能夠為系統(tǒng)是否滿足一些關(guān)鍵的正確性性質(zhì)作出了可靠保證。

形式化驗證中的模型檢測和程序驗證是他研究的兩個重要方向，他付出了很多心血，做出了重大貢獻(xiàn)。說起模型檢測問題，其實就是研究如何驗證系統(tǒng)模型正確性的研究領(lǐng)域。他著力研究概率模型檢測的算法、可判定性和計算復(fù)雜性，并獲得了一些基礎(chǔ)性理論成果。在模型檢測算法上，他以獨立作者身份給出了關(guān)于連續(xù)時間馬爾可夫過程時序邏輯的兩個基礎(chǔ)模型檢測算法，并發(fā)表在國際著名形式化驗證學(xué)術(shù)會議FOSSACS、HSCC上。其中發(fā)表在HSCC上的論文獲得了最佳學(xué)生論文獎。在可判定性和計算復(fù)雜性理論方面，他著力研究離散時間馬爾可夫過程上關(guān)于互模擬等價關(guān)系的可判定性和計算復(fù)雜性，并以獨立作者或主要貢獻(xiàn)者身份在國際著名理論計算機(jī)科學(xué)學(xué)術(shù)會議ICALP、FSTTCS上發(fā)表多篇重要論文。

相對于模型檢測，程序驗證是研究如何驗證程序正確性的方向。關(guān)于程序驗證問題，他在程序終止性以及運行時間驗證方面取得諸多基礎(chǔ)性理論成果，并發(fā)表在國際頂級形式化方法、程序語言理論以及人工智能學(xué)術(shù)會議POPL、CAV、IJCAI上。他作為主要貢獻(xiàn)者與合作者提出了分級上鞅在同時帶有惡意非確定性與友善非確定性概率程序上的定義，并給出了線性分級上鞅的合成算法以及相關(guān)的計算復(fù)雜性，進(jìn)而為帶有非確定性的概率程序終止性與期望運行時間驗證提供了一個堅實的理論基礎(chǔ)；同時，他在該成果中證明了分級上鞅可以導(dǎo)出有限步內(nèi)不終止概率的指數(shù)衰減性（POPL 2016，TOPLAS 2018）。他通過實代數(shù)幾何中的一些數(shù)學(xué)定理以及半正定規(guī)劃給出了概率程序上合成多項式分級上鞅的一個高效算法（CAV 2016）。他針對概率程序的資源消耗給出了一個基礎(chǔ)的驗證算法（IJCAI 2018）。最后，他將分級函數(shù)推廣至非概率遞歸程序，進(jìn)而通過線性規(guī)劃以及實代數(shù)幾何上的一些定理給出了一個輸出非概率遞歸程序精確運行時間的驗證算法；該算法可以有效地輸出很多經(jīng)典遞歸算法（如歸并排序、最近點對算法等）的精確非多項式運行時間 (CAV 2017)；同時，他基于一元遞歸關(guān)系針對隨機(jī)遞歸算法給出了一個驗證精確期望運行時間的高效算法；該算法可以在線性時間內(nèi)輸出一個由隨機(jī)遞歸算法導(dǎo)出的遞歸關(guān)系的精確期望運行時間（CAV 2017）。

創(chuàng)新是科研的靈魂。符鴻飛覺得在形式化驗證這個研究領(lǐng)域的創(chuàng)新有三種成果：一是通過復(fù)雜的數(shù)學(xué)方法解決一個已經(jīng)被提出的公認(rèn)難題；二是創(chuàng)新可以通過提出新的理論概念、并通過充實的依據(jù)說明提出的概念具有理論或?qū)嶋H上的意義；三是創(chuàng)新還可以通過將理論成果應(yīng)用到大規(guī)模工業(yè)系統(tǒng)中，以驗證實際系統(tǒng)中的一些關(guān)鍵性質(zhì)。

作為導(dǎo)師，他在上海交通大學(xué)帶領(lǐng)博士生進(jìn)行形式化方法深入研究，并教授《離散數(shù)學(xué)》、《程序語言理論》等與形式化驗證相關(guān)的課程。同時，他與博士導(dǎo)師Joost-Pieter Katoen教授、博士后合作導(dǎo)師Krishnendu Chatterjee教授以及一些國內(nèi)著名學(xué)者保持合作關(guān)系，致力于推進(jìn)形式化驗證的更大發(fā)展。

對從事教學(xué)與科研的專家來說，科學(xué)研究最重要的就是傳承，科研成果的取得需要一代代科研人在承上啟下中再創(chuàng)新高。符鴻飛真切地希望通過自己悉心傳教，盡早培養(yǎng)出一批具有扎實專業(yè)知識基礎(chǔ)、能夠獨立自主開展科研工作的學(xué)生，進(jìn)一步探索如何將所創(chuàng)理論更多地應(yīng)用于豐富的實踐中，推動學(xué)科專業(yè)邁向科學(xué)的頂峰。