一句话：为可参数化内存模型的组合符号执行平台提供新形式基础，并在 Rocq 中机器化。
组合符号执行（CSE）工具常用分离逻辑（SL）做组合验证，或用不正确性分离逻辑（ISL）找缺陷；Gillian 是唯一可参数化内存模型的 CSE 平台，实践显示自定义内存模型能带来灵活性与性能优势，但该方向缺乏令人满意的形式基础。本文受 Gillian 启发，为内存模型参数化的 CSE 平台提出新形式基础。该基础在交互式定理证明器 Rocq 中机器化，并实例化到包括 C 与 CHERI 在内的多种内存模型；与以往仅覆盖 SL 的参数化工作不同，它同时覆盖 SL 与 ISL，且基于 SL/ISL 的标准定义（含函数规约有效性），以支持与其他标准工具可靠互操作。
Multiple successful compositional symbolic execution (CSE) tools and platforms exploit separation logic (SL) for compositional verification and/or incorrectness separation logic (ISL) for compositional bug-finding, including VeriFast, Viper, Gillian, CN, and Infer-Pulse. Previous work on the Gillian platform, the only CSE platform that is parametric on the memory model, meaning that it can be instantiated to different memory models, suggests that the ability to use custom memory models allows for more flexibility in supporting analysis of a wide range of programming languages, for implementing custom automation, and for improving performance. However, the literature lacks a satisfactory formal foundation for memory-model-parametric CSE platforms. In this paper, inspired by Gillian, we provide a new formal foundation for memory-model-parametric CSE platforms. Our foundation advances the state of the art in four ways. First, we mechanise our foundation (in the interactive theorem prover Rocq). Second, we validate our foundation by instantiating it to a broad range of memory models, including models for C and CHERI. Third, whereas previous memory-model-parametric work has only covered SL analyses, we cover both SL and ISL analyses. Fourth, our foundation is based on standard definitions of SL and ISL (including definitions of function specification validity, to ensure sound interoperation with other tools and platforms also based on standard definitions).
@article{paperbot2993,
title = {Compositional Symbolic Execution for the Next 700 Memory Models},
author = {Andreas Lööw and Seung Hoon Park and Daniele Nantes-Sobrinho and Sacha-Élie Ayoun and Opale Sjöstedt and Philippa Gardner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763151}
}