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