{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:55:24Z","timestamp":1781884524273,"version":"3.54.5"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"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>\n                  <jats:p>Using Isabelle\/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operation whose soundness and completeness is easy to verify. Then, we prove the original formulation of the explain operation to be equal to our version. Finally, we refine this data structure to Imperative HOL, enabling us to export efficient imperative code. The formalisation provides a stepping stone towards the verification of proof-producing congruence closure algorithms which are a core ingredient of Satisfiability Modulo Theories (SMT) solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_15","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:55Z","timestamp":1753789675000},"page":"261-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Simplified and\u00a0Verified: A Second Look at\u00a0a\u00a0Proof-Producing Union-Find Algorithm"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0222-6858","authenticated-orcid":false,"given":"Lukas","family":"Stevens","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-8117-2659","authenticated-orcid":false,"given":"Rebecca","family":"Ghidini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"15_CR1","unstructured":"Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley (1974). ISBN 0-201-00029-6"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Types for Proofs and Programs, pp. 34\u201350. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_3","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A versatile and industrial-strength SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 13243, pp. 415\u2013442, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Bouton, T., Caminha B.\u00a0de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Conference on Automated Deduction, pp. 151\u2013156, Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Theorem Proving in Higher Order Logics, pp. 134\u2013149. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_14","DOI":"10.1007\/978-3-540-71067-7_14"},{"issue":"3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10817-017-9431-7","volume":"62","author":"A Chargu\u00e9raud","year":"2019","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. 62(3), 331\u2013365 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9431-7","journal-title":"J. Autom. Reason."},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Conchon, S., Filli\u00e2tre, J.C.: A persistent union-find data structure. In: Workshop on ML, pp. 37\u201346. Association for Computing Machinery, New York (2007). https:\/\/doi.org\/10.1145\/1292535.1292541","DOI":"10.1145\/1292535.1292541"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Flatt, O., Coward, S., Willsey, M., Tatlock, Z., Panchekha, P.: Small proofs from congruence closure. In: Formal Methods in Computer-Aided Design, pp. 75\u201383. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_13","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_13"},{"issue":"5","key":"15_CR9","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1145\/364099.364331","volume":"7","author":"BA Galler","year":"1964","unstructured":"Galler, B.A., Fisher, M.J.: An improved equivalence algorithm. Commun. ACM 7(5), 301\u2013303 (1964). https:\/\/doi.org\/10.1145\/364099.364331","journal-title":"Commun. ACM"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Guttmann, W.: Verifying the correctness of disjoint-set forests with Kleene relation algebras. In: Relational and Algebraic Methods in Computer Science, pp. 134\u2013151. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_9","DOI":"10.1007\/978-3-030-43520-2_9"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Haslbeck, M.P.L., Lammich, P.: Refinement with time - refining the run-time of algorithms in Isabelle\/HOL. In: Interactive Theorem Proving, pp. 20:1\u201320:18 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.20","DOI":"10.4230\/LIPIcs.ITP.2019.20"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Certified Programs and Proofs. LNCS, pp. 131\u2013146. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_9","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Computer Aided Verification, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"1","key":"15_CR14","doi-asserted-by":"publisher","first-page":"48","DOI":"10.2307\/2033241","volume":"7","author":"JB Kruskal","year":"1956","unstructured":"Kruskal, J.B.: On the shortest spanning subtree of a graph and the traveling salesman problem. Proc. Am. Mathe. Soc. 7(1), 48\u201350 (1956). https:\/\/doi.org\/10.2307\/2033241","journal-title":"Proc. Am. Mathe. Soc."},{"issue":"4","key":"15_CR15","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10817-017-9437-1","volume":"62","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: Refinement to imperative HOL. J. Autom. Reason. 62(4), 481\u2013503 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9437-1","journal-title":"J. Autom. Reason."},{"key":"15_CR16","unstructured":"Lammich, P., Meis, R.: A separation logic framework for imperative HOL. Archive of Formal Proofs (2012). ISSN 2150-914x. https:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html. Formal proof development"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Interactive Theorem Proving, pp. 166\u2013182. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12","DOI":"10.1007\/978-3-642-32347-8_12"},{"key":"15_CR18","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Proofs and refutations, and Z3. In: International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008). https:\/\/ceur-ws.org\/Vol-418\/paper10.pdf"},{"issue":"2","key":"15_CR19","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":"15_CR20","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Term Rewriting and Applications, pp. 453\u2013468. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33","DOI":"10.1007\/978-3-540-32033-3_33"},{"issue":"4","key":"15_CR21","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007). https:\/\/doi.org\/10.1016\/j.ic.2006.08.009","journal-title":"Inf. Comput."},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms: a biased survey. In: Automated Technology for Verification and Analysis, pp. 25\u201353. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_2","DOI":"10.1007\/978-3-030-59152-6_2"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"15_CR24","unstructured":"Noschinski, L.: Graph theory. Archive of Formal Proofs (2013). ISSN 2150-914x. https:\/\/isa-afp.org\/entries\/Graph_Theory.html. Formal proof development"},{"issue":"1","key":"15_CR25","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/S11786-014-0183-Z","volume":"9","author":"L Noschinski","year":"2015","unstructured":"Noschinski, L.: A graph library for Isabelle. Math. Comput. Sci. 9(1), 23\u201339 (2015). https:\/\/doi.org\/10.1007\/S11786-014-0183-Z","journal-title":"Math. Comput. Sci."},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Conference on Automated Deduction. LNAI, vol. 11716, pp. 495\u2013507. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Stevens, L., Nipkow, T.: A verified decision procedure for orders in Isabelle\/HOL. In: Automated Technology for Verification and Analysis, pp. 127\u2013143. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-88885-5_9"},{"issue":"2","key":"15_CR28","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215\u2013225 (1975). https:\/\/doi.org\/10.1145\/321879.321884","journal-title":"J. ACM"},{"issue":"2","key":"15_CR29","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/62.2160","volume":"31","author":"RE Tarjan","year":"1984","unstructured":"Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245\u2013281 (1984). https:\/\/doi.org\/10.1145\/62.2160","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:25:56Z","timestamp":1781882756000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}