SOSP，全稱ACM Symposium on Operating Systems Principles，是ACM組織在計算機系統領域的旗艦型會議，也是目前國際計算機系統領域的頂級會議。SOSP頂會對論文的質量和數量要求極高，每年只錄用30-40篇左右正式會議論文，通常錄取率約19%（今年錄取率是 18.78%），要求投稿方具有基礎性貢獻、領導性影響和堅實的系統背景。阿里云入選論文主要介紹了云基礎設施網絡自研DNS權威解析的形式化驗證工作，該工作對于提升阿里云DNS產品穩定性、正確性具有重要意義。DNS全稱Domain Name System，即域名解析系統。它將用戶輸入的網址（例如：www.example.com）翻譯為網絡設備可以讀懂的地址（例如：1.2.3.4），從而引導用戶連接到正確的網絡服務器。DNS系統的正確性和穩定性，是網絡可否成功服務廣大互聯網用戶的先決條件。

針對解析程序，傳統的測試技術只能保證測試用例部分正確性，并不能完整的、無死角的確保程序沒有 bug，阿里云形式化驗證工作則實現了無死角發現程序中全部bug，并降低了對人工輔助的大量依賴，目前，該驗證技術在業界已首次實際應用于規?；渴鸬漠a品代碼程序中，并高效完成了2000多行代碼的DNS權威解析程序的驗證，為云上客戶提供了真實有力的穩定性保障。

論文鏈接參考：https://dl.acm.org/doi/10.1145/3600006.3613153