一句话：提出在线输入语法合成辅助符号执行的方法 Lase，通过语法导向搜索与 token 级语法合成生成合法输入，提升解析与功能代码覆盖。
符号执行分析具有复杂输入格式的程序时，难以生成能通过输入检查并进入功能代码的合法输入；基于 token 的符号执行只能部分缓解。本文提出 Lase，一种在线输入语法合成辅助的符号执行方法：在符号执行中动态合成输入语法，采用面向输入语法的搜索策略，优先选择能覆盖更多语法规则的路径；并提出 token 级语法合成方法，在保证效率的同时提升合成语法的精度与完整性。在真实解析程序上的实验表明，Lase 能提高解析代码覆盖率，生成更多合法输入并显著提高功能代码覆盖率；与最先进的语法合成方法相比，其在多数基准程序上学到的语法具有更好的精度和召回率。
Symbolic execution faces the challenge of generating valid inputs when analyzing the program with complex input formats. Token-based symbolic execution can partially tackle this challenge but is still doomed by the difficulty of passing input checking and failing to analyze the code after input checking. We propose Lase , an online input grammar synthesis aided symbolic execution method, to generate valid inputs for improving the effectiveness of symbolic execution. Inside Lase , we propose an input grammar-oriented search strategy and a token-level grammar synthesis method. The search strategy selects the paths to cover more syntax rules in priority. The token-level grammar synthesis improves the synthesized grammar’s precision and completeness while ensuring efficiency. The experimental results on real-world parsing programs with complex input grammars demonstrate that Lase can improve the coverage of parsing code and generate more valid inputs to improve the coverage of functionality code significantly. Furthermore, compared with the state-of-the-art grammar synthesis methods, the grammars learned by Lase have better precision and recall on most benchmark programs.
@article{paperbot3819,
title = {Online Input Grammar Synthesis Aided Symbolic Execution},
author = {Ke Ma and Yunlai Luo and Zhenbang Chen and Weijiang Hong and Yufeng Zhang and Ji Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798243}
}