一句话：提出共享溯因与双溯因循环加速，使基于双溯因的形状分析更精确、更高效且单阶段健全。
基于双溯因（biabduction）的形状分析是一种组合式验证与分析技术，可在复杂链表等数据结构存在时证明内存安全。该文解决其两个开放问题：其一，原分析虽路径敏感，却无法合并相关分支的安全需求，导致需要额外健全性检查并降低精度；作者扩展底层符号执行，提出共享溯因框架，为相关计算分支维护公共前置条件。其二，既有实现将循环加速从前向分析分别作用于前条件与后条件，可能产生不精确甚至不健全、不构成循环不变式的结果；作者提出双溯因循环加速，显式构造并检查候选循环不变式，并引入形状外推启发式，利用列表类数据结构的局部性联合加速前后条件。由于新技术在一个分析阶段即健全，不再需要先产生契约再验证的第二阶段。实验证实其精度与运行时间均优于先前技术。
Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis; two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis’ precision. We extend the underlying symbolic execution and propose a framework for shared abduction where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose biabductive loop acceleration , which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called shape extrapolation . This heuristic takes advantage of locality in the handling of list-like data structures (which are the most common data structures found in low-level code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques; both in terms of precision and runtime of the analysis. This work extends the conference paper [32].
@inproceedings{SextlRVZ25,
title = {Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration},
author = {Florian Sextl and Adam Rogalewicz and Tomáš Vojnar and Florian Zuleger},
booktitle = {TOPLAS},
year = {2026},
doi = {10.1145/3844730}
}