{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:22:24Z","timestamp":1779074544014,"version":"3.51.4"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about <jats:italic>algebraic data types<\/jats:italic> (ADTs) and compositions of <jats:italic>structural recursions<\/jats:italic>. Modern theorem provers provide <jats:italic>structural induction<\/jats:italic> for such reasoning, but a structural induction on the original theorem is often insufficient for many equivalence theorems. In such cases, one has to invent a set of lemmas, prove these lemmas by additional induction, and use these lemmas to prove the original theorem. There is, however, a lack of systematic understanding of what lemmas are needed for inductive proofs and how these lemmas can be synthesized automatically. This paper presents <jats:italic>directed lemma synthesis<\/jats:italic>, an effective approach to automating equivalence proofs by discovering critical lemmas using program synthesis techniques. We first identify two <jats:italic>induction-friendly<\/jats:italic> forms of propositions that give formal guarantees to the progress of the proof. We then propose two tactics that synthesize and apply lemmas, thereby transforming the proof goal into induction-friendly forms. Both tactics reduce lemma synthesis to a set of independent and typically small program synthesis problems that can be efficiently solved. Experimental results demonstrate the effectiveness of our approach: Compared to state-of-the-art equivalence checkers employing heuristic-based lemma enumeration, directed lemma synthesis saves 95.47% runtime on average and solves 38 more tasks over an extended version of the standard benchmark set.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_28","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"538-557","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Proving Functional Program Equivalence via\u00a0Directed Lemma Synthesis"],"prefix":"10.1007","author":[{"given":"Yican","family":"Sun","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruyi","family":"Ji","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Fang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuanlin","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingfei","family":"Xiong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: Verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, pp. 1\u201310 (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"28_CR3","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8","DOI":"10.1007\/978-3-540-74113-8"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-20615-8_23","volume-title":"Intelligent Computer Mathematics","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 333\u2013337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_23"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semi-ring constraints. SMT@ IJCAR 20, 88\u201397 (2012)","DOI":"10.29007\/qqvt"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-66167-4_10","volume-title":"Frontiers of Combining Systems","author":"S Cruanes","year":"2017","unstructured":"Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172\u2013188. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"Danvy, O., Nielsen, L.R.: Defunctionalization at work. In: Proceedings of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 162\u2013174. PPDP 2001, Association for Computing Machinery, New York, NY, USA (2001). https:\/\/doi.org\/10.1145\/773184.773202","DOI":"10.1145\/773184.773202"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0A\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-030-25540-4_19","volume-title":"Computer Aided Verification","author":"N Gavrilenko","year":"2019","unstructured":"Gavrilenko, N., Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 355\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-030-53518-6_8","volume-title":"Intelligent Computer Mathematics","author":"M Hajd\u00fa","year":"2020","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 123\u2013137. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8"},{"key":"28_CR12","doi-asserted-by":"publisher","unstructured":"Ireland, A., Bundy, A.: Productive Use of Failure in Inductive Proof, pp. 79\u2013111. Springer Netherlands, Dordrecht (1996). https:\/\/doi.org\/10.1007\/978-94-009-1675-3_3","DOI":"10.1007\/978-94-009-1675-3_3"},{"key":"28_CR13","doi-asserted-by":"publisher","unstructured":"Ji, R., Zhao, Y., Xiong, Y., Wang, D., Zhang, L., Hu, Z.: Decomposition-based synthesis for applying divide-and-conquer-like algorithmic paradigms. ACM Trans. Program. Lang. Syst. (2024). https:\/\/doi.org\/10.1145\/3648440, just Accepted","DOI":"10.1145\/3648440"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-14052-5_21","volume-title":"Interactive Theorem Proving","author":"M Johansson","year":"2010","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 291\u2013306. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_21"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. Proc. ACM Prog. Lang. 2(POPL), 1\u201333 (2017)","DOI":"10.1145\/3158142"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"28_CR17","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/s10009-015-0366-1","volume":"18","author":"NP Lopes","year":"2016","unstructured":"Lopes, N.P., Monteiro, J.: Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int. J. Softw. Tools Technol. Transfer 18, 359\u2013374 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"28_CR18","unstructured":"Luick, D., et al.: ZKSMT: A VM for proving SMT theorems in zero knowledge. Cryptology ePrint Archive (2023)"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification: Fundamental Issues in Computer Science, vol. 14, pp. 35\u201356. Springer, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_2","DOI":"10.1007\/978-94-011-1793-7_2"},{"key":"28_CR20","doi-asserted-by":"publisher","unstructured":"Milovan\u010devi\u0107, D., Kun\u010dak, V.: Proving and disproving equivalence of functional programming assignments. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591258","DOI":"10.1145\/3591258"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"28_CR23","doi-asserted-by":"publisher","unstructured":"Murali, A., Pe\u00f1a, L., Blanchard, E., L\u00f6ding, C., Madhusudan, P.: Model-guided synthesis of inductive lemmas for FOL with least fixpoints. Proc. ACM Program. Lang. 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563354","DOI":"10.1145\/3563354"},{"key":"28_CR24","doi-asserted-by":"publisher","unstructured":"Murali, A., Pe\u00f1a, L., Jhala, R., Madhusudan, P.: Complete first-order reasoning for properties of functional programs. Proc. ACM Program. Lang. 7(OOPSLA2) (2023). https:\/\/doi.org\/10.1145\/3622835","DOI":"10.1145\/3622835"},{"issue":"2","key":"28_CR25","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979). https:\/\/doi.org\/10.1145\/357073.357079","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-030-51054-1_30","volume-title":"Automated Reasoning","author":"G Passmore","year":"2020","unstructured":"Passmore, G., Cruanes, S., Ignatovich, D., Aitken, D., Bray, M., Kagan, E., Kanishev, K., Maclean, E., Mometto, N.: The Imandra automated reasoning system (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 464\u2013471. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_30"},{"key":"28_CR27","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers (2000)"},{"key":"28_CR28","unstructured":"Pierce, B.C., Casinghino, C., Gaboardi, M., Greenberg, M., Hri\u0163cu, C., Sj\u00f6berg, V., Yorgey, B.: Software foundations, p.\u00a016 (2010). http:\/\/www.cis.upenn.edu\/bcpierce\/sf\/current\/index.html"},{"key":"28_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-030-29436-6_28","volume-title":"Automated Deduction \u2013 CADE 27","author":"G Reger","year":"2019","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 477\u2013494. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_28"},{"key":"28_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"28_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-81688-9_6","volume-title":"Computer Aided Verification","author":"E Singher","year":"2021","unstructured":"Singher, E., Itzhaky, S.: Theory exploration powered by deductive synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 125\u2013148. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_6"},{"key":"28_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-28756-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Sonnex","year":"2012","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407\u2013421. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28"},{"key":"28_CR33","doi-asserted-by":"publisher","unstructured":"Sun, Y., Ji, R., Fang, J., Jiang, X., Chen, M., Xiong, Y.: Artifact for FM paper: proving Functional program equivalence via directed lemma. Synthesis (2024). https:\/\/doi.org\/10.5281\/zenodo.12532389","DOI":"10.5281\/zenodo.12532389"},{"key":"28_CR34","unstructured":"Sun, Y., Ji, R., Fang, J., Jiang, X., Chen, M., Xiong, Y.: Proving functional program equivalence via directed lemma synthesis (2024). https:\/\/arxiv.org\/abs\/2405.11535"},{"key":"28_CR35","volume-title":"Liquid Haskell: Haskell as a theorem prover","author":"N Vazou","year":"2016","unstructured":"Vazou, N.: Liquid Haskell: Haskell as a theorem prover. University of California, San Diego (2016)"},{"key":"28_CR36","doi-asserted-by":"crossref","unstructured":"VK, H.G., Shoham, S., Gurfinkel, A.: Solving constrained horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022)","DOI":"10.1145\/3498722"},{"key":"28_CR37","unstructured":"Wand, D.: Superposition: types and induction. Ph.D. thesis, Saarland University (2017)"},{"key":"28_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-030-30048-7_35","volume-title":"Principles and Practice of Constraint Programming","author":"W Yang","year":"2019","unstructured":"Yang, W., Fedyukovich, G., Gupta, A.: Lemma synthesis for automating induction over algebraic data types. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 600\u2013617. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30048-7_35"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:07:40Z","timestamp":1725934060000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}