软件学报

作者：冯维直，刘嘉祥，张立军，吴志林

单位：冯维直，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,刘嘉祥，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019002,张立军，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,吴志林，基础软件与系统重点实验室(中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004904

关键词：形式化方法;递归函数;可满足性模理论;归纳推理;引理合成;约束霍恩子句

基金：中国科学院战略性先导科技专项 (XDA0320101)

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

来源：2026年第2期

《软件学报》期刊编辑部

查看软件学报杂志2026年第2期