5月31日上午，應基礎軟件國家工程研究中心的邀請，美國西密歇根大學的楊子江副教授到軟件所進行學術交流，并作題為“Scalable Symbolic Execution”的學術報告。學術報告會由劉劍副研究員主持。

報告中，楊教授針對符號執行技術進行了系統介紹，符號執行技術是一種有效的測試用例生成技術，且能達到一定邊界深度范圍的路徑覆蓋。楊教授介紹到，目前符號執行技術的應用受到路徑爆炸的限制，因為程序的路徑數往往以執行中的分支數呈指數級增長，因此，如何解決好符號執行中路徑爆炸是軟件系統可信領域中一個重要而熱門研究點。

在報告中，楊教授主要介紹了其團隊最近提出的一種緩解符號執行的路徑爆炸問題的方法。該方法主要通過刪減相同子路徑的分析來減少冗余的路徑遍歷，從而有效的緩解路徑爆炸。在講到裁剪冗余路徑時，他強調了其團隊的方法并不會裁剪任何可能產生錯誤的路徑，即這種方法能保證在裁剪路徑之前能發現的錯誤在裁剪路徑之后同樣能發現。同時，他還對符號執行技術的應用提出了自己的見解。

報告結束后，與會人員就符號執行技術、軟件安全和可信等問題與楊教授進行了深入廣泛的交流。

楊子江現任美國西密歇根大學計算機科學系（Computer Science at Western Michigan University）副教授，也是美國密歇根大學（University of Michigan）的客座教授。他的研究領域包括軟件系統的安全和可信，主要包括基于形式化方法的復雜系統建模、分析以及驗證方法的研究。其研究工作目前受美國國家科學基金（NSF）、美海軍研究辦公室（Office of Naval Research）等多個方面的資助。

楊子江副教授作報告

報告會現場