一句话：提出统一的组合式符号执行方法，构建 JaVerT 2.0，首次为 JavaScript 支持基于双向溯因的自动组合测试。
论文旨在弥合经典符号执行与基于分离逻辑的组合式程序推理之间的鸿沟。作者提出一种开发组合式符号执行工具的统一方法，并据此构建 JaVerT 2.0：一个不简化 JavaScript 语义的符号分析工具，支持全程序符号测试、验证，以及首次实现的基于双向溯因的自动组合测试。其元理论采用模块化方式构建，简化证明并指导实现；对符号执行错误的显式处理可为开发者提供反馈，并引导双向溯因执行中的资源推断。作者在多个 JavaScript 数据结构库上评估性能，展示了全程序符号测试的可扩展性、相对现有 JavaScript 验证的改进，以及 JavaScript 自动组合测试的可行性。
We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.
@article{paperbot657,
title = {JaVerT 2.0: compositional symbolic execution for JavaScript},
author = {José Fragoso Santos and Petar Maksimović and Gabriela Sampaio and Philippa Gardner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290379}
}