一句话：提出 Goblin，基于带语义约束的上下文无关文法，借助 SMT 求解器生成满足上下文敏感约束的测试输入。
基于语法的模糊测试在具有高度结构化输入格式的软件系统中能有效发现缺陷，但许多现有工具依赖上下文无关文法（CFG）表示输入结构，而 CFG 往往不足以刻画真实输入中常见的上下文敏感约束；应用专用 fuzzer 虽能处理这类约束，却缺乏适应新应用的通用性。Goblin 接受带语义约束标注的 CFG，生成既符合文法又满足约束的输入。其显著特点是通过外部 SMT 求解器支持任意 SMT 理论中的约束。受 DPLL 风格 SAT 求解器启发，Goblin 具有解可靠性、解完备性和反驳可靠性的形式保证。作者通过与先前工作比较，并将 Goblin 集成到基于语法的网络协议模糊测试器中进行了评估。
Grammar-based fuzzers have been effective at identifying bugs in software systems with highly structured input formats (e.g., XML). Many existing grammar-based fuzzers rely on context-free grammars (CFGs) to represent input structure; however, CFGs are often insufficient to capture the context-sensitive constraints common in real-world inputs. While application-specific fuzzers can often handle such constraints, they lack the generality needed to adapt to new applications. We present Goblin, a new input generation tool that addresses this gap. Given a context-free grammar annotated with semantic constraints, Goblin generates inputs that both conform to the grammar and satisfy the constraints. A distinguishing feature of Goblin is its support—via an external SMT solver—for constraints expressed in arbitrary SMT theories. Inspired by DPLL-style SAT solvers, Goblin enjoys formal guarantees of solution soundness, solution completeness, and refutation soundness. We evaluate Goblin by comparing it with prior work and by integrating it into a grammar-based network protocol fuzzer.