AI 中文总结
本文针对符号执行工具自身正确性缺乏形式审查的问题，对带路径合并的符号执行进行形式化处理，以Java Ranger为对象证明其转换的健全性，确立其路径合并过程可保留程序语义。
AI 中文摘要
符号执行在软件可靠性中发挥着关键作用，用于发现漏洞、生成测试用例并提供正确性保障，尤其适用于安全关键系统。然而，符号执行工具自身的正确性却很少受到形式审查，通常仅通过在多个程序上评估工具行为的经验方式来确立，这使得工具本身可能引入不健全性，进而可能使其生成的验证结果失效，破坏其本应提供的保障。本文针对这一缺口，对带有路径合并的符号执行进行形式化处理，路径合并是一种优化方法，通过将分支代码区域总结为析取约束而非独立探索每条路径，来缓解路径爆炸问题。具体而言，本文以Java Ranger为研究对象，这是一款针对Java程序的路径合并工具，它通过一系列代码转换，将命令式Java代码逐步转换为形式逻辑语言。本文对每一次转换进行形式化，并针对简化版Java具体语义证明其健全性，从而确立Java Ranger的路径合并过程可保留程序语义。
英文摘要
Symbolic execution plays a critical role in software reliability, as they are used to find bugs, generate test cases, and provide correctness guarantees, particularly for safety-critical systems. Yet their own correctness is rarely subject to formal scrutiny, as it is typically established empirically by evaluating tool behavior across many programs. This leaves open the possibility that the tools themselves introduce unsoundness, potentially invalidating the verification results they produce and undermining the very guarantees they are meant to provide. In this paper, we address this gap by providing the formal treatment of symbolic execution with path-merging, an optimization that improves path explosion by summarizing branching code regions into disjunctive constraints rather than exploring each path independently. Specifically, we target Java Ranger, a path-merging tool for Java programs that progressively transforms imperative Java code toward the language of formal logic through a series of code transformations. We formalize each of these transformations and prove their soundness with respect to a simplified version of the Java concrete semantics, establishing that Java Ranger's path-merging process preserves program semantics.
CommentsAddress review comments, update affliations
