美國《技術評論》（Technology Review）雜誌最近評選出2011年度十大新興技術，“不會崩潰的代碼”（Crash-Proof Code）名列其中（見http://www.technologyreview.com/tr10/）。這項技術是指用邏輯推理的方法來進行程序驗證，以構造高可信的安全攸關軟件。
《技術評論》主要介紹了澳大利亞國家信息與通信技術研究中心（NICTA）2009年完成的對可以實際應用的操作係統內核seL4的驗證。它證明了seL4能可靠地運行，絕不會崩潰，並且其運行始終滿足對它的安全性質要求，隻要該證明的各項前提（又稱為信任基，即trusted computing base）得到滿足。
係統軟件作為直接控製計算硬件係統的基礎軟件，它本身的缺陷更容易導致整個計算係統的失控。2010年被用來攻擊伊朗的大量工業設施，甚至包括伊朗布什爾核電廠的令人聞之色變的“超級蠕蟲病毒”Stuxnet就是通過操作係統漏洞開展攻擊。該病毒利用Windows操作係統的4個“zero-day attack”，獲取係統控製權，然後攻擊運行於係統之上的西門子WinCC/PCS 7 SCADA控製軟件。攻擊成功後，離心機運轉速度失控，直至癱瘓。為最大限度達到破壞效果，病毒還同時向監控設備發送偽造的“正常數據”，令監控人員無法及時察覺。構造crash-proof的係統內核則有望從根本上杜絕這一類攻擊。
《技術評論》在有關這項技術的報導中提到，從事這方麵研究的還有我校馮新宇教授、微軟Redmond研究院Chris Hawblitzel研究員和耶魯大學邵中教授（我校大師講席教授）。
邵中教授、馮新宇教授和中科大－耶魯高可信軟件聯合研究中心的其他研究人員等在2008年也驗證了一個小的操作係統內核。雖然該內核僅僅是一個非常小的實驗性係統，功能比seL4要少得多，但該驗證工作所依賴的信任基比seL4的驗證也要小得多，因為它基於一種非常基礎的元邏輯並且所有的代碼都經過驗證，而seL4的底層部分C代碼和600行彙編代碼並沒有驗證，屬於所依賴的信任基部分（信任基越小，驗證工作的可靠性就越高）。
《技術評論》是美國專業的科技商業雜誌，創刊於1899年，由麻省理工學院主辦，以推介、評析科技創新為宗旨，展示最新科技成果及其商業潛能，內容涉及互聯網、通訊、計算機技術、能源、新材料、生物醫學和商務科技等領域。
《技術評論》主編Jason Pontin去年6月在廣州演講時說：“幾乎每年我們都會選出十大新興技術。我們認為這些技術能夠改變世界，這些技術能夠商業化，能夠投入到當今市場中，促進市場的發展。… 例如，幾年前我們評選出手機，認為它是相當先進的技術，今天大家已看到確有很多人在使用手機。2005年我們選擇了合成生物，合成生物今天也在快速發展。”
（中科大－耶魯高可信軟件聯合研究中心供稿）
