中科大－耶魯高可信軟件聯(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ū)域中。

　　論文第一作者梁紅瑾是中國科大計算機(jī)科學(xué)與技術(shù)學(xué)院博士一年級學(xué)生，她與馮新宇教授等的論文提出了一種驗證并發(fā)程序變換的一般方法，首次將并發(fā)程序邏輯中的依賴-保證條件（rely-guarantee conditions）引入到傳統(tǒng)的程序模擬關(guān)系（simulation）中，成功地解決了對驗證提供模塊化支持的難題，并將這種方法應(yīng)用于編譯優(yōu)化、并發(fā)數(shù)據(jù)結(jié)構(gòu)的實(shí)現(xiàn)和并發(fā)垃圾收集等算法的正確性驗證。審稿人對論文的貢獻(xiàn)給予了充分肯定，他們分別指出：“我感到這篇文章很吸引人。結(jié)合模擬關(guān)系與依賴-保證推理的想法看起來很不錯，而且我在別處都沒有見過……這項工作能提供一種漂亮的統(tǒng)一理論，用于驗證并發(fā)程序變換。”“并發(fā)系統(tǒng)的精化問題的研究非常具有挑戰(zhàn)性，這篇文章則向這個領(lǐng)域邁出了很好的一步。”“一個能夠同時支持運(yùn)行時系統(tǒng)驗證和編譯器驗證的邏輯將非常有用。這篇文章展示了這樣一個邏輯，并且看起來是一種非常普適的、自然的方法。”

　　作為聯(lián)合研究中心的研究進(jìn)入國際一流水平的又一體現(xiàn)是，聯(lián)合研究中心邵中教授（我校大師講席教授）和馮新宇教授被介紹國際新興技術(shù)的期刊列為國際上從事新興技術(shù)“防崩潰代碼”（Crash-Proof Code）的主要研究人員。防崩潰代碼是美國麻省理工學(xué)院主辦的、頗具影響力的Technology Review雜志（中文版名字為《科技創(chuàng)業(yè)》）今年第6期評選出的2011年度十大新興技術(shù)之一。這項技術(shù)是指用邏輯推理的方法來進(jìn)行程序驗證，以構(gòu)造高可信的安全攸關(guān)軟件。《科技創(chuàng)業(yè)》主要介紹了澳大利亞國家信息與通信技術(shù)研究中心（NICTA）2009年完成的對可以實(shí)際應(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年也驗證了一個小的實(shí)驗性的操作系統(tǒng)內(nèi)核以展示相關(guān)理論和技術(shù)上的突破。雖然該內(nèi)核比seL4小得多，但得益于他們提出的“開放式驗證框架理論”的方法學(xué)、硬件中斷驗證技術(shù)和匯編程序驗證技術(shù)，內(nèi)核的所有代碼都得到了驗證。

　　中科大－耶魯高可信軟件聯(lián)合研究中心成立于2008年10月，以我校計算機(jī)學(xué)院軟件安全實(shí)驗室的力量為主體，耶魯大學(xué)邵中教授主持的Flint小組給予技術(shù)支持和研究合作。雙方的合作研究始于2004年，根據(jù)研究領(lǐng)域和研究隊伍的特點(diǎn)，當(dāng)初就把目標(biāo)設(shè)定為建設(shè)領(lǐng)域內(nèi)國際一流的研究中心。經(jīng)歷以耶魯為主合作發(fā)表、以我方為主合作發(fā)表和我方能夠獨(dú)自發(fā)表國際一流水平論文這樣幾個階段，聯(lián)合研究中心已經(jīng)奠定了堅實(shí)的研究基礎(chǔ)，形成了以海外引進(jìn)的馮新宇教授為學(xué)術(shù)帶頭人的研究團(tuán)隊。

51CTO評論員：如果此次的論文不存在任何學(xué)術(shù)抄襲等丑聞存在，確實(shí)是目前中國科學(xué)研究的一種進(jìn)步。在經(jīng)歷蘇聯(lián)式教育影響幾十年后，我國高校的自主研究落后亞洲其他各國。高校領(lǐng)導(dǎo)與教授，更多的是陷入權(quán)利爭奪和追求個人金錢的陷阱里。教授走穴講課收取高額培訓(xùn)費(fèi)，女學(xué)生被教授潛規(guī)則等等確實(shí)讓中國高校成為了一個患了齲齒的“象牙塔”。

中國不少程序員覺得自己的技術(shù)水平低。而似乎所有的編程語言之父不是出自歐美就是日本，基本上沒有中國人的份。這需要中國的高校真正走上科研的道路，玩點(diǎn)正兒八經(jīng)的技術(shù)活。而不是成為學(xué)位和畢業(yè)證的印刷機(jī)。

【編輯推薦】

1. 中國第一代程序員列傳
2. 51CTO專項調(diào)研：2011年中國Web開發(fā)工具選擇和使用情況
3. 福昕：中國土著十年暗戰(zhàn)Adobe
4. 中國應(yīng)用開源腳本語言PHP的水平如何?
5. 中國的網(wǎng)頁設(shè)計為什么這么爛？