2023年12月2日,2023年度CCF中國軟件大會軟件程序語義深度理解前沿進展論壇成功召開。
本次論壇由南京大學卜磊老師和國防科技大學陳振邦老師主持,計算機研究與發展期刊代表侯麗珊老師致辭,旨在反映程序語義理解及其應用相關研究前沿進展與實踐,并推動國內相關研究向深度發展。論壇邀請了來自清華大學、南京大學、國防科技大學、電子科技大學和航天科技集團的相關領域學者作為論壇嘉賓,主要關注抽象解釋、靜態分析、符號執行等相關技術的最新進展。此外,論壇還邀請了中國科學院大學張健教授做題為“程序分析與測試數據生成”的特邀報告。本次論壇得到了學術界和工業界相關領域研究者的廣泛參與,座無虛席。
???+
本次論壇分兩個階段舉行。論壇第一階段由南京大學卜磊老師主持,包括一個特邀報告和2篇論文報告,并在每位論壇嘉賓報告結束后為其頒發證書。首先是由中國科學院大學張健教授的題為“程序分析與測試數據生成”的精彩主題報告。張健老師首先介紹了自動推理和邏輯公式可滿足性的內容,并講述了自己在不同描述語言下的約束滿足問題以及模型計數等領域的研究,其次講述了程序分析和測試的相關內容,并講述了自己在符號執行、靜態分析以及程序性能估算等方面的前瞻性研究,最后張老師對程序分析的相關技術作出總結并提出了自己的感想和思考,表示程序分析大有可為。接下來由國防科技大學陳立前老師做題為“抽象解釋及其應用進展研究”的報告,主要闡述抽象解釋理論的概述和發展、基于抽象解釋的程序分析、基于抽象解釋的可信人工智能以及對未來研究方向的展望等內容。最后是由南京大學譚添老師做題為“Java指針分析:上下文敏感技術的發展”的報告,通過相關例子呈現了針對java程序的指針分析過程,并呈現了指針分析中上下文敏感可擴展性差的問題,提出在指針流圖上通過三種模式消除指向圖上指向匯合點的邊并額外添加指向分叉點的邊的方式,達到不使用上下文也能達到上下文敏感的效果。
論壇第二階段由國防科技大學陳振邦老師主持。首先由清華大學的王明哲系統性地介紹了模糊測試中典型的靜態插樁方法,并對靜態插樁的優化方向進行展望。隨后來自電子科技大學的宋書瑋介紹智能合約中Gas優化面臨的主要挑戰,并回顧基于預先定義的Pattern等智能合約優化方法,最后總結了智能合約可擴展性的未來研究方向。隨后來自航天科技集團502所的李超介紹了原子性違反的缺陷檢測技術,通過路徑不敏感的數據流分析進行訪問交錯模式的匹配,后續通過收集路徑約束裁剪不可行路徑,最后對中斷驅動型程序靜態分析框架等進行展望。最后是來自南京大學的周彭介紹基于多線程并行的符號執行引擎設計與實現,線程間通過竊取實現負載均衡,并共享基于反例約束求解的約束緩存,提高了符號執行的效率。最后論壇圓滿結束。