在軟件定義一切的時(shí)代，軟件使能的系統(tǒng)遍布在人類(lèi)社會(huì)的各個(gè)方面、在不同程度發(fā)揮著重要的作用，軟件可信保障既是迫切需求又是重要挑戰(zhàn).對(duì)軟件的語(yǔ)義及其行為空間進(jìn)行深入理解是軟件可信保障的重要依據(jù)與前提.然而，隨著計(jì)算機(jī)技術(shù)的快速發(fā)展與應(yīng)用的日趨普及，軟件系統(tǒng)規(guī)模和復(fù)雜性持續(xù)增大，如何對(duì)大規(guī)模、復(fù)雜軟件系統(tǒng)的語(yǔ)義進(jìn)行理解，并指導(dǎo)軟件分析、測(cè)試、驗(yàn)證乃至優(yōu)化活動(dòng)是當(dāng)前領(lǐng)域關(guān)注的重要問(wèn)題.特別是在當(dāng)前開(kāi)源時(shí)代下，如何對(duì)大規(guī)模代碼高效構(gòu)建準(zhǔn)確的語(yǔ)義認(rèn)知，并基于相關(guān)認(rèn)知與理解進(jìn)行后續(xù)自動(dòng)化分析，具有重要意義.

為反映程序語(yǔ)義理解及其應(yīng)用相關(guān)研究前沿進(jìn)展與實(shí)踐，并推動(dòng)國(guó)內(nèi)相關(guān)研究向深度發(fā)展，我們組織“程序語(yǔ)義深度理解前沿進(jìn)展”專(zhuān)題，邀請(qǐng)領(lǐng)域?qū)＜覍?duì)抽象解釋、符號(hào)執(zhí)行、模糊測(cè)試等程序語(yǔ)義理解的重要技術(shù)手段進(jìn)行綜述總結(jié)與進(jìn)展報(bào)告，并圍繞JAVA 指針?lè)治?、中斷?qū)動(dòng)代碼原子性違反檢測(cè)、智能合約優(yōu)化等領(lǐng)域重要問(wèn)題進(jìn)行專(zhuān)題討論.

抽象解釋是程序分析的基礎(chǔ)理論之一，在安全攸關(guān)軟件的分析與驗(yàn)證方面發(fā)揮了重要的作用，近年來(lái)也被拓展到人工智能、安全等領(lǐng)域.陳立前等人的“抽象解釋及其應(yīng)用研究進(jìn)展”一文對(duì)近年來(lái)抽象解釋在理論本身、基于抽象解釋的可信人工智能和智能合約、信息安全及量子計(jì)算等的可信保證等方向的最新進(jìn)展進(jìn)行了系統(tǒng)、全面的總結(jié)、分析和介紹.

符號(hào)執(zhí)行是一種重要的程序分析技術(shù)，常用于程序的測(cè)試輸入生成和缺陷自動(dòng)檢測(cè)，近年來(lái)受到了學(xué)術(shù)界和工業(yè)界的廣泛關(guān)注.然而，符號(hào)執(zhí)行仍面臨路徑空間爆炸和約束求解這兩個(gè)關(guān)鍵挑戰(zhàn)，嚴(yán)重阻礙了符號(hào)執(zhí)行的進(jìn)一步發(fā)展和應(yīng)用.針對(duì)相關(guān)問(wèn)題，周彭和左志強(qiáng)的“基于多線(xiàn)程并行的符號(hào)執(zhí)行引擎設(shè)計(jì)與實(shí)現(xiàn)”一文提出了一種基于多線(xiàn)程并行化的符號(hào)執(zhí)行解決方案，將路徑探索過(guò)程均攤到多個(gè)工作線(xiàn)程中，在線(xiàn)程間共享約束求解信息，提高求解緩存的命中率，實(shí)現(xiàn)符號(hào)執(zhí)行效率的提升.

近年來(lái)，模糊測(cè)試技術(shù)在工業(yè)界大規(guī)模系統(tǒng)的測(cè)試中得到廣泛應(yīng)用.王明哲等人的 “模糊測(cè)試中的靜態(tài)插樁技術(shù)”一文對(duì)模糊測(cè)試以及模糊測(cè)試背景下的靜態(tài)插樁技術(shù)進(jìn)行介紹，分別介紹了安全特性強(qiáng)化插樁和導(dǎo)向信息收集插樁這兩類(lèi)靜態(tài)插樁技術(shù)及其應(yīng)用場(chǎng)景，并且結(jié)合最新的工業(yè)界和學(xué)術(shù)界的成果對(duì)不同目的的靜態(tài)插樁技術(shù)進(jìn)行解釋剖析.

指針?lè)治鍪浅绦蚍治鲋械囊粋€(gè)經(jīng)典問(wèn)題，得到了相關(guān)領(lǐng)域長(zhǎng)期以來(lái)的持續(xù)關(guān)注.譚添等人的 “Java 指針?lè)治鼍C述”一文系統(tǒng)綜述了Java 指針?lè)治龅闹匾獌?nèi)容：指針?lè)治鏊惴ā⑸舷挛拿舾小⒍褜?duì)象抽象、復(fù)雜語(yǔ)言特性處理、非全程序指針?lè)治觯⑾到y(tǒng)性地梳理和討論了近年來(lái)Java 指針?lè)治龅难芯窟M(jìn)展，為相關(guān)研究人員快速了解相關(guān)問(wèn)題領(lǐng)域提供參考.

航天嵌入式軟件是一種典型安全攸關(guān)軟件，原子性違反是航天嵌入式軟件中斷并發(fā)缺陷中的一類(lèi)常見(jiàn)缺陷類(lèi)型.研究適合航天嵌入式軟件原子性違反的檢測(cè)方法具有重要實(shí)用價(jià)值.于婷婷等人的“中斷驅(qū)動(dòng)型航天嵌入式軟件原子性違反檢測(cè)方法”一文針對(duì)航天嵌入式軟件中原子性違反缺陷的表現(xiàn)形式開(kāi)展了實(shí)證研究，并基于實(shí)證研究得到的特征，提出了一種精度高、效率高的中斷驅(qū)動(dòng)型程序原子性違反靜態(tài)檢測(cè)方法.

智能合約的Gas 優(yōu)化是近年來(lái)的一個(gè)熱點(diǎn)問(wèn)題.宋書(shū)緯等人的“智能合約Gas 優(yōu)化綜述”一文針對(duì)智能合約的執(zhí)行過(guò)程中的Gas 消耗問(wèn)題進(jìn)行了系統(tǒng)性的調(diào)研與分析，對(duì)Gas 優(yōu)化相關(guān)工作與研究方向進(jìn)行了整理與總結(jié)，為智能合約開(kāi)發(fā)者，以及智能合約執(zhí)行優(yōu)化等相關(guān)方向的研究者，提供了指引與展望.

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