|
中科大－耶魯高可信軟件聯(lián)合研究中心梁紅瑾、馮新宇和付明的論文“一種用于驗證并發(fā)程序變換的基于依賴-保證的模擬關(guān)系”（A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations）被第39屆編程語言原理國際會議（ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages，簡稱POPL）錄用。此前，中國大陸尚無任何單位以第一作者單位的身份在POPL上發(fā)表過論文，中國科大是第一個以第一單位在POPL上發(fā)表論文的高校和科研院所。 POPL是編程語言領(lǐng)域歷史最久、水平最高的國際會議，它是討論編程語言和編程系統(tǒng)最新突破的最主要論壇，內(nèi)容涵蓋編程語言的理論、編程語言的設(shè)計、編譯器技術(shù)、程序分析、程序驗證、可信軟件等眾多研究領(lǐng)域。國際期刊和會議的各種分區(qū)方法都把POPL放在該領(lǐng)域的最高區(qū)域中。 論文第一作者梁紅瑾是中國科大計算機科學(xué)與技術(shù)學(xué)院博士一年級學(xué)生，她與馮新宇教授等的論文提出了一種驗證并發(fā)程序變換的一般方法，首次將并發(fā)程序邏輯中的依賴-保證條件（rely-guarantee conditions）引入到傳統(tǒng)的程序模擬關(guān)系（simulation）中，成功地解決了對驗證提供模塊化支持的難題，并將這種方法應(yīng)用于編譯優(yōu)化、并發(fā)數(shù)據(jù)結(jié)構(gòu)的實現(xiàn)和并發(fā)垃圾收集等算法的正確性驗證。審稿人對論文的貢獻給予了充分肯定，他們分別指出：“我感到這篇文章很吸引人。結(jié)合模擬關(guān)系與依賴-保證推理的想法看起來很不錯，而且我在別處都沒有見過……這項工作能提供一種漂亮的統(tǒng)一理論，用于驗證并發(fā)程序變換。”“并發(fā)系統(tǒng)的精化問題的研究非常具有挑戰(zhàn)性，這篇文章則向這個領(lǐng)域邁出了很好的一步。”“一個能夠同時支持運行時系統(tǒng)驗證和編譯器驗證的邏輯將非常有用。這篇文章展示了這樣一個邏輯，并且看起來是一種非常普適的、自然的方法。” 作為聯(lián)合研究中心的研究進入國際一流水平的又一體現(xiàn)是，聯(lián)合研究中心邵中教授（我校大師講席教授）和馮新宇教授被介紹國際新興技術(shù)的期刊列為國際上從事新興技術(shù)“防崩潰代碼”（Crash-Proof Code）的主要研究人員。防崩潰代碼是美國麻省理工學(xué)院主辦的、頗具影響力的Technology Review雜志（中文版名字為《科技創(chuàng)業(yè)》）今年第6期評選出的2011年度十大新興技術(shù)之一。這項技術(shù)是指用邏輯推理的方法來進行程序驗證，以構(gòu)造高可信的安全攸關(guān)軟件。《科技創(chuàng)業(yè)》主要介紹了澳大利亞國家信息與通信技術(shù)研究中心（NICTA）2009年完成的對可以實際應(yīng)用的操作系統(tǒng)內(nèi)核seL4的驗證。《科技創(chuàng)業(yè)》在有關(guān)這項技術(shù)的報導(dǎo)中提到，從事這方面研究的還有我校馮新宇教授、微軟Redmond研究院Chris Hawblitzel研究員和耶魯大學(xué)邵中教授。 NICTA的研發(fā)主要展示驗證大型系統(tǒng)軟件的可行性。他們驗證了seL4的大部分代碼，但由于相關(guān)理論和技術(shù)的欠缺，不得不放棄對一些最底層的關(guān)鍵代碼的驗證，包括底層部分C代碼和600行匯編代碼，因而可靠性保證尚不夠徹底。邵中教授和馮新宇教授的研究則主要針對系統(tǒng)軟件驗證中的關(guān)鍵理論和技術(shù)。他們帶領(lǐng)聯(lián)合研究中心的研究人員等在2008年也驗證了一個小的實驗性的操作系統(tǒng)內(nèi)核以展示相關(guān)理論和技術(shù)上的突破。雖然該內(nèi)核比seL4小得多，但得益于他們提出的“開放式驗證框架理論”的方法學(xué)、硬件中斷驗證技術(shù)和匯編程序驗證技術(shù)，內(nèi)核的所有代碼都得到了驗證。 中科大－耶魯高可信軟件聯(lián)合研究中心成立于2008年10月，以我校計算機學(xué)院軟件安全實驗室的力量為主體，耶魯大學(xué)邵中教授主持的Flint小組給予技術(shù)支持和研究合作。雙方的合作研究始于2004年，根據(jù)研究領(lǐng)域和研究隊伍的特點，當初就把目標設(shè)定為建設(shè)領(lǐng)域內(nèi)國際一流的研究中心。經(jīng)歷以耶魯為主合作發(fā)表、以我方為主合作發(fā)表和我方能夠獨自發(fā)表國際一流水平論文這樣幾個階段，聯(lián)合研究中心已經(jīng)奠定了堅實的研究基礎(chǔ)，形成了以海外引進的馮新宇教授為學(xué)術(shù)帶頭人的研究團隊。 新聞來源:中國科大新聞網(wǎng) |
