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

542 软件学报 2026 年第 37 卷第 2 期

[56] Hajdú M, Kovács L, Rawson M, Voronkov A. The Vampire approach to induction (short paper). In: Proc. of the 2022 Workshop on
Practical Aspects of Automated Reasoning Co-located with the 11th Int’l Joint Conf. on Automated Reasoning. Haifa: CEUR Workshop
Proc., 2022.
[57] Hajdu M. Automating inductive reasoning with recursive functions [Ph.D. Thesis]. Wien: Technische Universität Wien, 2020.
[58] Bradley AR. SAT-based model checking without unrolling. In: Proc. of the 12th Int’l Conf. on Verification, Model Checking, and
Abstract Interpretation. Austin: Springer, 2011. 70–87. [doi: 10.1007/978-3-642-18275-4_7]
[59] Een N, Mishchenko A, Brayton R. Efficient implementation of property directed reachability. In: Proc. of the 2011 Int’l Conf. on Formal
Methods in Computer-aided Design. Austin: FMCAD Inc, 2011. 125–134.
[60] Komuravelli A, Gurfinkel A, Chaki S, Clarke EM. Automatic abstraction in SMT-based unbounded software model checking. In: Proc. of
the 25th Int’l Conf. Computer Aided Verification. Saint Petersburg: Springer, 2013. 846–862. [doi: 10.1007/978-3-642-39799-8_59]
[61] Komuravelli A, Gurfinkel A, Chaki S. SMT-based model checking for recursive programs. In: Proc. of the 26th Int’l Conf. on Computer
Aided Verification. Vienna: Springer, 2014. 17–34. [doi: 10.1007/978-3-319-08867-9_2]
[62] Hojjat H, Rümmer P. The Eldarica Horn solver. In: Proc. of the 2018 Formal Methods in Computer Aided Design. Austin: IEEE, 2018.
1–7. [doi: 10.23919/FMCAD.2018.8603013]
[63] Gambhir S, Kunčak V. CHC solvers in stainless: Work in progress. 2024. https://www.sci.unich.it/hcvs24/papers/HCVS2024_paper_9.
pdf
[64] Suter P, Dotta M, Kuncak V. Decision procedures for algebraic data types with abstractions. In: Proc. of the 37th Annual ACM
SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Madrid: ACM, 2010. 199–210. [doi: 10.1145/1706299.1706325]
[65] Pham TH, Whalen MW. An improved unrolling-based decision procedure for algebraic data types. In: Proc. of the 5th Int’l Conf. on
Verified Software: Theorie, Tools, Experiments. Menlo Park: Springer, 2014. 129–148. [doi: 10.1007/978-3-642-54108-7_7]
[66] Pham TH, Gacek A, Whalen MW. Reasoning about algebraic data types with abstractions. Journal of Automated Reasoning, 2016, 57(4):
281–318. [doi: 10.1007/s10817-016-9368-2]
[67] Pham TH, Whalen MW. RADA: A tool for reasoning about algebraic data types with abstractions. In: Proc. of the 9th Joint Meeting on
Foundations of Software Engineering. Saint Petersburg: ACM, 2013. 611–614. [doi: 10.1145/2491411.2494597]
[68] Voronkov A, Kovács L. Vampire team. 2025. https://vprover.github.io/team.html
[69] Reger G, Suda M, Voronkov A, Kovács L, Bhayat A, Gleiss B, Hajdu M, Hozzova P, Rath J, Rawson M, Schoisswohl J. Vampire
4.8—SMT system description. 2023. https://smt-comp.github.io/2023/system-descriptions/Vampire.pdf
[70] Rümmer P, Hojjat H, Kuncak V. Disjunctive interpolants for Horn-clause verification. In: Proc. of the 25th Int’l Conf. on Computer
Aided Verification. Saint Petersburg: Springer, 2013. 347–363. [doi: 10.1007/978-3-642-39799-8_24]
[71] Ernst G, Morales JF. CHC-COMP 2024 report. 2024. https://chc-comp.github.io/2024/CHC-COMP%202024%20Report%20-%20HCSV.
pdf
[72] Bjørner N. SPACER and Z3: Accessible, reliable model checking as theorem proving. 2018. https://www.microsoft.com/en-us/research/
blog/spacer-and-z3-accessible-reliable-model-checking-as-theorem-proving/
[73] Feng WZ, Liu YC, Liu JX, Jansen DN, Zhang LJ, Wu ZL. Formally verifying arithmetic chisel designs for all bit widths at once. In: Proc.
of the 61st ACM/IEEE Design Automation Conf. San Francisco: ACM, 2024. 213. [doi: 10.1145/3649329.3657311]
[74] Rosen KH. Discrete Mathematics and Its Applications. 8th ed., New York: McGraw-Hill, 2019.

作者简介
冯维直, 博士生, CCF 学生会员, 主要研究领域为形式化方法, 计算机软硬件验证.
刘嘉祥, 博士, 副研究员, CCF 专业会员, 主要研究领域为形式化方法, 程序验证, 神经网络验证.
张立军, 博士, 研究员, 主要研究领域为概率模型检测, 协议验证, 学习算法, 自动驾驶系统验证.
吴志林, 博士, 研究员, CCF 高级会员, 主要研究领域为计算逻辑, 自动机理论, 计算机软硬件基础设施的形式化验证.