Page 29 - 《软件学报》2026年第2期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2026,37(2):508−542 [doi: 10.13328/j.cnki.jos.007560] [CSTR: 32375.14.jos.007560] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
带递归定义的 SMT 公式求解技术综述

冯维直 1,2,3 , 刘嘉祥 1,2 , 张立军 1,2,3 , 吴志林 1,2,3

1
(基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190)
(计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190)
2
3
(中国科学院大学, 北京 100049)
通信作者: 吴志林, E-mail: wuzl@ios.ac.cn

摘 要: 带有递归数据结构, 如列表 (list) 和二叉树 (tree) 等数据类型的程序, 在计算机领域被广泛使用. 程序验证
问题通常将程序转换为可满足性模理论 (satisfiability modulo theories, SMT) 公式进行求解. 递归数据结构通常会
转换为代数数据类型 (algebraic data type, ADT) 和整数等混合理论的一阶逻辑公式. 另外, 为表示递归数据结构的
性质, 程序中通常需要包含递归函数, 递归函数在 SMT 中则需要通过包含量词和未解释函数的断言来表示. 关注
带有 ADT 和递归函数这两类递归定义 SMT 公式的求解方法. 从 SMT 求解器、自动定理证明器和约束霍恩子句
(constrained Horn clause, CHC) 求解器这 3 方面对现有技术进行梳理和介绍. 同时, 对主流的求解工具进行统一实
验对比, 探究现有求解工具和技术在各类问题上的优势和缺陷, 尝试寻找潜在的优化方向, 为研究者提供有价值的
分析和参考.
关键词: 形式化方法; 递归函数; 可满足性模理论; 归纳推理; 引理合成; 约束霍恩子句
中图法分类号: TP301

中文引用格式: 冯维直, 刘嘉祥, 张立军, 吴志林. 带递归定义的SMT公式求解技术综述. 软件学报, 2026, 37(2): 508–542. http://
www.jos.org.cn/1000-9825/7560.htm
英文引用格式: Feng WZ, Liu JX, Zhang LJ, Wu ZL. Survey on Solving SMT Formulas with Recursive Definitions. Ruan Jian Xue
Bao/Journal of Software, 2026, 37(2): 508–542 (in Chinese). http://www.jos.org.cn/1000-9825/7560.htm

Survey on Solving SMT Formulas with Recursive Definitions
1,2
FENG Wei-Zhi 1,2,3 , LIU Jia-Xiang , ZHANG Li-Jun 1,2,3 , WU Zhi-Lin 1,2,3
1
(Key Laboratory of Systems Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China)
2
(State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China)
3
(University of Chinese Academy of Sciences, Beijing 100049, China)
Abstract: Programs with recursive data structures, such as list and tree, are widely used in computer science. Program verification
problems are often translated into satisfiability modulo theories (SMT) formulas for solving. Recursive data structures are usually converted
into first-order logic formulas combining algebraic data types (ADTs) and other theories such as integers. To express properties of
recursive data structures, programs often include recursive functions, which in SMT are represented using assertions with quantifiers and
uninterpreted functions. This study focuses on solving methods for SMT formulas with both ADTs and recursive functions. Existing
techniques are reviewed from three perspectives: SMT solvers, automated theorem provers, and constrained Horn clause (CHC) solvers.
Furthermore, the study conducts unified experiments to compare state-of-the-art tools on different benchmarks. It investigates the
advantages and limitations of existing solving tools and techniques on various types of problems and explores potential optimization
directions, providing valuable analyses and references for researchers.
Key words: formal method; recursive function; satisfiability modulo theories (SMT); inductive reasoning; lemma synthesis; constrained Horn
clause (CHC)

* 基金项目: 中国科学院战略性先导科技专项 (XDA0320101)
收稿时间: 2025-02-18; 修改时间: 2025-07-23; 采用时间: 2025-09-26; jos 在线出版时间: 2025-12-10
CNKI 网络首发时间: 2025-12-11