一句话：提出支持 magic wand 与 isorecursive 谓词的溯因推断，为 Viper 推断循环不变式及辅助操作，可覆盖 80% 以上内存安全规约。
分离逻辑验证器（如 Viper）能证明堆操作与并发程序性质，但依赖大量前后条件和循环不变式标注。现有 bi-abduction 不支持 magic wand，且采用 equirecursive 而非 SMT 验证器常用的 isorecursive 谓词解释，难以推断列表段以外结构的遍历规约。本文提出新的溯因推断，可推断结合用户定义谓词与 magic wand 的循环不变式，记录待遍历部分与剩余结构，以便遍历后保持整个结构所有权；并首次推断操作谓词和 wand 所需的辅助操作。作者在 Viper 中实现，评估显示可为多样化基准中超过 80% 的内存安全验证规约完成推断。
Program verifiers based on separation logic, such as Gillian, VeriFast, and Viper, allow one to prove complex properties of heap-manipulating, concurrent programs. These tools automate a large part of the proof search, but require a substantial amount of annotations such as method pre- and postconditions and loop invariants. Inference techniques such as bi-abduction can alleviate this burden, but existing techniques are too restrictive to be used in expressive program verifiers. In particular, existing bi-abduction techniques do not support the magic wand connective, so that inference for iterative traversals of structures beyond list segments is limited. Moreover, they rely on an equirecursive interpretation of predicates, instead of the isorecursive interpretation used by most SMT-based verifiers. In this paper, we present a novel abductive inference that addresses these limitations. It infers loop invariants that combine user-defined predicates with magic wands to keep track of the part of a data structure still to be traversed and the remainder of the data structure, such that ownership of the entire structure is retained after the traversal. Moreover, our abduction technique is the first to infer the auxiliary operations required by verifiers to manipulate predicates and wands. We implemented our inference in Viper; our evaluation shows that our approach can infer over 80% of the specifications required to verify memory safety of a diverse benchmark set.
@article{paperbot12119,
title = {Abductive Inference of Separation Logic Specifications with Isorecursive User-Defined Predicates and Magic Wands},
author = {Nicolas Klose and Peter Müller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839488}
}