前言

在軟件定義一切的時代，軟件使能的系統遍布在人類社會的各個方面、在不同程度發揮著重要的作用，軟件可信保障既是迫切需求又是重要挑戰.對軟件的語義及其行為空間進行深入理解是軟件可信保障的重要依據與前提.然而，隨著計算機技術的快速發展與應用的日趨普及，軟件系統規模和復雜性持續增大，如何對大規模、復雜軟件系統的語義進行理解，并指導軟件分析、測試、驗證乃至優化活動是當前領域關注的重要問題.特別是在當前開源時代下，如何對大規模代碼高效構建準確的語義認知，并基于相關認知與理解進行后續自動化分析，具有重要意義.

為反映程序語義理解及其應用相關研究前沿進展與實踐，并推動國內相關研究向深度發展，我們組織“程序語義深度理解前沿進展”專題，邀請領域專家對抽象解釋、符號執行、模糊測試等程序語義理解的重要技術手段進行綜述總結與進展報告，并圍繞JAVA 指針分析、中斷驅動代碼原子性違反檢測、智能合約優化等領域重要問題進行專題討論.

抽象解釋是程序分析的基礎理論之一，在安全攸關軟件的分析與驗證方面發揮了重要的作用，近年來也被拓展到人工智能、安全等領域.陳立前等人的“抽象解釋及其應用研究進展”一文對近年來抽象解釋在理論本身、基于抽象解釋的可信人工智能和智能合約、信息安全及量子計算等的可信保證等方向的最新進展進行了系統、全面的總結、分析和介紹.

符號執行是一種重要的程序分析技術，常用于程序的測試輸入生成和缺陷自動檢測，近年來受到了學術界和工業界的廣泛關注.然而，符號執行仍面臨路徑空間爆炸和約束求解這兩個關鍵挑戰，嚴重阻礙了符號執行的進一步發展和應用.針對相關問題，周彭和左志強的“基于多線程并行的符號執行引擎設計與實現”一文提出了一種基于多線程并行化的符號執行解決方案，將路徑探索過程均攤到多個工作線程中，在線程間共享約束求解信息，提高求解緩存的命中率，實現符號執行效率的提升.

近年來，模糊測試技術在工業界大規模系統的測試中得到廣泛應用.王明哲等人的 “模糊測試中的靜態插樁技術”一文對模糊測試以及模糊測試背景下的靜態插樁技術進行介紹，分別介紹了安全特性強化插樁和導向信息收集插樁這兩類靜態插樁技術及其應用場景，并且結合最新的工業界和學術界的成果對不同目的的靜態插樁技術進行解釋剖析.

指針分析是程序分析中的一個經典問題，得到了相關領域長期以來的持續關注.譚添等人的 “Java 指針分析綜述”一文系統綜述了Java 指針分析的重要內容：指針分析算法、上下文敏感、堆對象抽象、復雜語言特性處理、非全程序指針分析，并系統性地梳理和討論了近年來Java 指針分析的研究進展，為相關研究人員快速了解相關問題領域提供參考.

航天嵌入式軟件是一種典型安全攸關軟件，原子性違反是航天嵌入式軟件中斷并發缺陷中的一類常見缺陷類型.研究適合航天嵌入式軟件原子性違反的檢測方法具有重要實用價值.于婷婷等人的“中斷驅動型航天嵌入式軟件原子性違反檢測方法”一文針對航天嵌入式軟件中原子性違反缺陷的表現形式開展了實證研究，并基于實證研究得到的特征，提出了一種精度高、效率高的中斷驅動型程序原子性違反靜態檢測方法.

智能合約的Gas 優化是近年來的一個熱點問題.宋書緯等人的“智能合約Gas 優化綜述”一文針對智能合約的執行過程中的Gas 消耗問題進行了系統性的調研與分析，對Gas 優化相關工作與研究方向進行了整理與總結，為智能合約開發者，以及智能合約執行優化等相關方向的研究者，提供了指引與展望.

深入理解程序語義是通向軟件可信保障的必由之路.希望本專題的出版能夠拋磚引玉，對系統軟件、軟件工程及其相關領域的研究人員有所幫助和啟發，以進一步促進相關研究.由于時間倉促、容量有限，本專題無法全面覆蓋相關領域的所有最新研究工作，敬請各位同行諒解和批評指正.衷心感謝《計算機研究與發展》提供了寶貴機會出版此專題論文! 衷心感謝各位作者、審稿專家和編輯部工作人員的全力支持和辛勤付出，使得本專題能順利出版!