论文标题
符号执行游戏语义
Symbolic Execution Game Semantics
论文作者
论文摘要
我们提出了一个框架，用于用外部（开放）方法象征性地执行和模型检查高阶程序。我们专注于客户图书馆范式，尤其是我们旨在与任何可定义的客户端检查库。我们将传统的符号执行技术与操作游戏语义结合起来，以构建捕获任意外部行为的符号执行语义。我们证明了符号语义是合理而完整的。这通过在递归和回调的深度上施加界限来产生有限的技术。我们在K框架中提供了技术的实现，并根据更高阶段的编码错误（例如重新进入错误）在自定义基准标准上展示其性能。
We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the K framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs.
