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

冯维直 等: 带递归定义的 SMT 公式求解技术综述 541

[30] Biere A, Heule M, van Maaren H, Walsh T. Handbook of Satisfiability. 2nd ed., Washington: IOS Press, 2021.
[31] Reynolds A, Kuncak V. Induction for SMT solvers. In: Proc. of the 16th Int’l Conf. on Verification, Model Checking, and Abstract
Interpretation. Mumbai: Springer, 2015. 80–98. [doi: 10.1007/978-3-662-46081-8_5]
[32] Suter P, Köksal AS, Kuncak V. Satisfiability modulo recursive programs. In: Proc. of the 18th Int’l Symp. on Static Analysis. Venice:
Springer, 2011. 298–315. [doi: 10.1007/978-3-642-23702-7_23]
[33] Blanc R, Kuncak V, Kneuss E, Suter P. An overview of the Leon verification system: Verification by translation to recursive functions.
In: Proc. of the 4th Workshop on Scala. Montpellier: ACM, 2013. 1. [doi: 10.1145/2489837.2489838]
[34] Hamza J, Voirol N, Kunčak V. System FR: Formalized foundations for the stainless verifier. Proc. of the ACM on Programming
Languages, 2019, 3(OOPSLA): 166. [doi: 10.1145/3360592]
[35] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL—A Proof Assistant for Higher-order Logic. Berlin, Heidelberg: Springer, 2002. [doi:
10.1007/3-540-45949-9]
[36] Kaufmann M, Manolios P, Moore JS. Computer-aided Reasoning: ACL2 Case Studies. New York: Springer, 2000. [doi: 10.1007/978-1-
4757-3188-0]
[37] Sonnex W, Drossopoulou S, Eisenbach S. Zeno: An automated prover for properties of recursive data structures. In: Proc. of the 18th Int’l
Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Tallinn: Springer, 2012. 407–421. [doi: 10.1007/978-3-642-
28756-5_28]
[38] Bundy A, Basin D, Hutter D, Ireland A. Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge: Cambridge University
Press, 2005.
[39] Kapur D, Subramaniam M. Using an induction prover for verifying arithmetic circuits. Int’l Journal on Software Tools for Technology
Transfer, 2000, 3(1): 32–65. [doi: 10.1007/PL00010808]
[40] Murali A, Peña L, Blanchard E, Löding C, Madhusudan P. Model-guided synthesis of inductive lemmas for FOL with least fixpoints.
Proc. of the ACM on Programming Languages, 2022, 6(OOPSLA2): 191. [doi: 10.1145/3563354]
[41] Hesketh JT. Using middle-out reasoning to guide inductive theorem proving [Ph.D. Thesis]. Edinburgh: University of Edinburgh, 1991.
[42] Johansson M, Dixon L, Bundy A. Dynamic rippling, middle-out reasoning and lemma discovery. In: Siegler S, Wasser N, eds.
Verification, Induction, Termination Analysis. Berlin, Heidelberg: Springer, 2010. 102–116. [doi: 10.1007/978-3-642-17172-7_6]
[43] Buchberger B. Theory exploration with theorema. Analele Universitatii Din Timisoara, Seria Matematica-Informatica, 2000, 38(2): 9–32.
[44] McCasland R, Bundy A, Autexier S. Automated discovery of inductive theorems. Studies in Logic, Grammar and Rhetoric, 2007, 10(23):
135–149.
[45] Yang WK, Fedyukovich G, Gupta A. Lemma synthesis for automating induction over algebraic data types. In: Proc. of the 25th Int’l
Conf. on Principles and Practice of Constraint Programming. Stamford: Springer, 2019. 600–617. [doi: 10.1007/978-3-030-30048-7_35]
[46] Sivaraman A, Sanchez-Stern A, Chen B, Lerner S, Millstein TD. Data-driven lemma synthesis for interactive proofs. Proc. of the ACM
on Programming Languages, 2022, 6(OOPSLA2): 143. [doi: 10.1145/3563306]
[47] Sun YC, Ji RY, Fang J, Jiang XL, Chen MS, Xiong YF. Proving functional program equivalence via directed lemma synthesis. In: Proc.
of the 26th Int’l Symp. Formal Methods. Milan: Springer, 2025. 538–557. [doi: 10.1007/978-3-031-71162-6_28]
[48] Reynolds A, Tinelli C, Goel A, Krstić S. Finite model finding in SMT. In: Proc. of the 25th Int’l Conf. Computer Aided Verification.
Saint Petersburg: Springer, 2013. 640–655. [doi: 10.1007/978-3-642-39799-8_42]
[49] Reynolds A, Tinelli C, Goel A, Krstić S, Deters M, Barrett C. Quantifier instantiation techniques for finite model finding in SMT. In:
Proc. of the 24th Int’l Conf. on Automated Deduction. Lake Placid: Springer, 2013. 377–391. [doi: 10.1007/978-3-642-38574-2_26]
[50] Reynolds A, Blanchette JC, Cruanes S, Tinelli C. Model finding for recursive functions in SMT. In: Proc. of the 8th Int’l Joint Conf. on
Automated Reasoning. Coimbra: Springer, 2016. 133–151. [doi: 10.1007/978-3-319-40229-1_10]
[51] Reger G, Voronkov A. Induction in saturation-based proof search. In: Proc. of the 27th Int’l Conf. on Automated Deduction. Natal:
Springer, 2019. 477–494. [doi: 10.1007/978-3-030-29436-6_28]
[52] Echenim M, Peltier N. Combining induction and saturation-based theorem proving. Journal of Automated Reasoning, 2020, 64(2):
253–294. [doi: 10.1007/s10817-019-09519-x]
[53] Hajdú M, Hozzová P, Kovács L, Schoisswohl J, Voronkov A. Induction with generalization in superposition reasoning. In: Proc. of the
13th Int’l Conf. on Intelligent Computer Mathematics. Bertinoro: Springer, 2020. 123–137. [doi: 10.1007/978-3-030-53518-6_8]
[54] Hajdu M, Hozzová P, Kovács L, Voronkov A. Induction with recursive definitions in superposition. In: Proc. of the 2021 Formal
Methods in Computer Aided Design. New Haven: IEEE, 2021. 1–10. [doi: 10.34727/2021/isbn.978-3-85448-046-4_34]
[55] Hozzová P, Kovács L, Voronkov A. Integer induction in saturation. In: Proc. of the 28th Int’l Conf. on Automated Deduction. Springer,
2021. 361–377. [doi: 10.1007/978-3-030-79876-5_21]