一句话：提出 IC3 启发的 Racer 算法，在 ADT 与 catamorphism 下求解 CHC，自动合成归纳不变式并保证找到不安全反例。
验证操作数据结构（如 Rust）的命令式程序时，验证条件常含代数数据类型（ADT），其归纳不变式需递归定义函数（RDF）表示抽象。该问题归约为同时含 ADT 与 RDF 的约束 Horn 子句（CHC）求解，但底层逻辑不可判定，使 IC3 类算法失去进展保证。本文提出 IC3 启发的 Racer 算法，对 ADT 与 catamorphism 类 RDF 求解 CHC，自动合成归纳不变式。核心是将 catamorphism 编码为 CHC（relationification）以学习归纳性质并保持不可满足性，同时用新抽象编码为 RDF 以展开递归定义，抽象保证理论可判定。Racer 在不可判定理论下仍保证进展，对不安全程序终止并给出反例；在 Z3 中实现且实验效果良好。
This work addresses the problem of verifying imperative programs that manipulate data structures, e.g., Rust programs. Data structures are usually modeled by Algebraic Data Types (ADTs) in verification conditions. Inductive invariants of such programs often require recursively defined functions (RDFs) to represent abstractions of data structures. From the logic perspective, this reduces to solving Constrained Horn Clauses (CHCs) modulo both ADT and RDF. The underlying logic with RDFs is undecidable. Thus, even verifying a candidate inductive invariant is undecidable. Similarly, IC3-based algorithms for solving CHCs lose their progress guarantee: they may not find counterexamples when the program is unsafe. We propose a novel IC3-inspired algorithm Racer for solving CHCs modulo ADT and RDF (i.e., automatically synthesizing inductive invariants, as opposed to only verifying them as is done in deductive verification). Racer ensures progress despite the undecidability of the underlying theory, and is guaranteed to terminate with a counterexample for unsafe programs. It works with a general class of RDFs over ADTs called catamorphisms. The key idea is to represent catamorphisms as both CHCs, via relationification , and RDFs, using novel abstractions . Encoding catamorphisms as CHCs allows learning inductive properties of catamorphisms, as well as preserving unsatisfiabilty of the original CHCs despite the use of RDF abstractions, whereas encoding catamorphisms as RDFs allows unfolding the recursive definition, and relying on it in solutions. Abstractions ensure that the underlying theory remains decidable. We implement our approach in Z3 and show that it works well in practice.
@article{paperbot1557,
title = {Solving constrained Horn clauses modulo algebraic data types and recursive functions},
author = {Hari Govind V K and Sharon Shoham and Arie Gurfinkel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498722}
}