一句话：提出 OCaml 库 Soteria，支持直接在源语言语义上构建高效、可组合、可靠的符号执行引擎。
符号执行（SE）工具常借助中间语言（IL）来支持多种源语言，以求复用性与效率，但这在性能、精度与语言特性支持之间引入了折衷。作者主张：为每种源语言直接构建 SE 引擎既更简单也更有效。为此他们提出 Soteria——一个轻量级 OCaml 库，让开发者以函数式风格编写直接作用于源语言语义的 SE 引擎，兼具可配置性、组合式推理与易于实现等优点。基于 Soteria，作者实现了 Soteria-Rust（首个支持 Rust 复杂别名模型 TreeBorrows 的 Rust 符号执行引擎）与 Soteria-C（面向 C 的组合式 SE 引擎）。二者在性能与发现缺陷数量上均与 Kani、Infer.Pulse、CBMC、Gillian-C 等先进工具相当或更优。作者还形式化了 Soteria 的理论基础并证明了其可靠性，表明无需 IL 的折衷亦可实现可靠、高效、精确且表达力强的符号执行。
Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach introduces trade-offs between performance, accuracy, and language feature support. We argue that building SE engines directly for each source language is both simpler and more effective. We present Soteria, a lightweight OCaml library for writing SE engines in a functional style, without compromising on performance, accuracy or feature support. Soteria enables developers to construct SE engines that operate directly over source-language semantics, offering configurability, compositional reasoning, and ease of implementation. Using Soteria, we develop Soteria-Rust, the first Rust SE engine supporting TreeBorrows (the intricate aliasing model of Rust), and Soteria-C, a compositional SE engine for C. Both tools are competitive with or outperform state-of-the-art tools such as Kani, Infer.Pulse, CBMC and Gillian-C in performance and the number of bugs detected. We formalise the theoretical foundations of Soteria and prove its soundness, demonstrating that sound, efficient, accurate, and expressive SE can be achieved without the compromises of ILs.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-08729,
title = {Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!},
author = {Sacha-Élie Ayoun and Opale Sjöstedt and Azalea Raad},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808306}
}