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