{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T11:30:20Z","timestamp":1771241420704,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T00:00:00Z","timestamp":1771200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T00:00:00Z","timestamp":1771200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["NI 491\/161"],"award-info":[{"award-number":["NI 491\/161"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present the first formal correctness proof of Edmonds\u2019 blossom shrinking algorithm for maximum cardinality matching in general graphs. We focus on formalising the mathematical structures and properties that allow the algorithm to run in worst-case polynomial running time. We formalise Berge\u2019s lemma, blossoms and their properties, and a mathematical model of the algorithm, showing that it is totally correct. We provide the first detailed proofs of many of the facts underlying the algorithm\u2019s correctness.<\/jats:p>","DOI":"10.1007\/s10817-026-09747-y","type":"journal-article","created":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T10:57:25Z","timestamp":1771239445000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Correctness Proof of Edmonds\u2019 Blossom Shrinking Algorithm"],"prefix":"10.1007","volume":"70","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8244-518X","authenticated-orcid":false,"given":"Mohammad","family":"Abdulaziz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4020-4334","authenticated-orcid":false,"given":"Kurt","family":"Mehlhorn","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,2,16]]},"reference":[{"key":"9747_CR1","doi-asserted-by":"publisher","first-page":"449","DOI":"10.4153\/CJM-1965-045-4","volume":"17","author":"J Edmonds","year":"1965","unstructured":"Edmonds, J.: Paths, trees, and flowers. Can. J. Math. 17, 449\u2013467 (1965). https:\/\/doi.org\/10.4153\/CJM-1965-045-4","journal-title":"Can. J. Math."},{"key":"9747_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","journal-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic."},{"key":"9747_CR3","doi-asserted-by":"publisher","first-page":"842","DOI":"10.1073\/pnas.43.9.842","volume":"43","author":"C Berge","year":"1957","unstructured":"Berge, C.: Two theorems in graph theory. Proc. Natl. Acad. Sci. 43, 842\u2013844 (1957). https:\/\/doi.org\/10.1073\/pnas.43.9.842","journal-title":"Proc. Natl. Acad. Sci."},{"key":"9747_CR4","unstructured":"Mehlhorn, K., N\u00e4her, S.: LEDA: A Platform for Combinatorial and Geometric Computing, (1999). http:\/\/www.mpi-sb.mpg.de\/%7Emehlhorn\/LEDAbook.html Accessed 2023-10-09"},{"key":"9747_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24488-9","author":"B Korte","year":"2012","unstructured":"Korte, B., Vygen, J.: Comb. Optim. (2012). https:\/\/doi.org\/10.1007\/978-3-642-24488-9","journal-title":"Comb. Optim."},{"key":"9747_CR6","unstructured":"Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency, (2003)"},{"key":"9747_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4230\/LIPIcs.MFCS.2019.1","volume":"138","author":"M Abdulaziz","year":"2019","unstructured":"Abdulaziz, M., Mehlhorn, K., Nipkow, T.: Trustworthy graph algorithms (invited paper). The 44th Int. Symp. Math. Found Comput. Sci (MFCS) 138, 1\u20131122 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.1","journal-title":"The 44th Int. Symp. Math. Found Comput. Sci (MFCS)"},{"key":"9747_CR8","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52, 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"9747_CR9","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, 23\u201339 (2015). https:\/\/doi.org\/10.1007\/S11786-014-0183-Z","journal-title":"Math. Comput. Sci."},{"key":"9747_CR10","doi-asserted-by":"publisher","unstructured":"Edmonds, C., Paulson, L.C.: Formal Probabilistic Methods for Combinatorial Structures using the Lov\u00e1sz Local Lemma. In: The 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 132\u2013146 (2024). https:\/\/doi.org\/10.1145\/3636501.3636946","DOI":"10.1145\/3636501.3636946"},{"key":"9747_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.48550\/arXiv.2302.13747","volume":"268","author":"M Abdulaziz","year":"2023","unstructured":"Abdulaziz, M., Madlener, C.: A formal analysis of ranking. The 14th Conference on Interactive Theorem Proving (ITP) 268, 1\u201318 (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.13747","journal-title":"The 14th Conference on Interactive Theorem Proving (ITP)"},{"key":"9747_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4230\/LIPICS.ITP.2024.3","volume":"309","author":"M Abdulaziz","year":"2024","unstructured":"Abdulaziz, M., Ammer, T.: A formal analysis of capacity scaling algorithms for minimum cost flows. 15th Int. Conference Inter. Theorem Prov. (ITP) 309, 1\u201319 (2024). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2024.3","journal-title":"15th Int. Conference Inter. Theorem Prov. (ITP)"},{"key":"9747_CR13","unstructured":"Isabelle-Graph-Library. Last accessed on 27\/05\/2025 (2024). https:\/\/github.com\/mabdula\/Isabelle-Graph-Library Accessed 2024-10-15"},{"key":"9747_CR14","unstructured":"Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic. PhD thesis, Technical University Munich (2009). http:\/\/mediatum2.ub.tum.de\/doc\/681651\/document.pdf. Accessed 2022-03-25"},{"key":"9747_CR15","doi-asserted-by":"crossref","unstructured":"Bondy, J.A., Murty, U.S.R.: Graph Theory, 1st edn. (2008)","DOI":"10.1007\/978-1-84628-970-5"},{"key":"9747_CR16","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1007\/s10817-018-9495-z","volume":"63","author":"M Abdulaziz","year":"2019","unstructured":"Abdulaziz, M., Paulson, L.C.: An isabelle\/HOL formalisation of green\u2019s theorem. J. Autom. Reason. 63, 763\u2013786 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9495-z","journal-title":"J. Autom. Reason."},{"key":"9747_CR17","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575688","author":"F van Doorn","year":"2023","unstructured":"van Doorn, F., Massot, P., Nash, O.: Formalising the h-principle and sphere eversion. The 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) (2023). https:\/\/doi.org\/10.1145\/3573105.3575688","journal-title":"The 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)"},{"key":"9747_CR18","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373833","author":"F Immler","year":"2020","unstructured":"Immler, F., Tan, Y.K.: The poincar\u00e9-bendixson theorem in isabelle\/HOL. The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) (2020). https:\/\/doi.org\/10.1145\/3372885.3373833","journal-title":"The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)"},{"key":"9747_CR19","first-page":"305","volume":"13","author":"G Lee","year":"2005","unstructured":"Lee, G.: Correctnesss of ford-fulkerson\u2019s maximum flow algorithm1. Formalized Mathematics 13, 305\u2013314 (2005)","journal-title":"Formalized Mathematics"},{"key":"9747_CR20","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-017-9442-4","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing network flow algorithms: a refinement approach in isabelle\/HOL. J. Autom. Reason. 62, 261\u2013280 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9442-4","journal-title":"J. Autom. Reason."},{"key":"9747_CR21","unstructured":"Maric, F., Spasic, M., Thiemann, R.: An Incremental Simplex Algorithm with Unsatisfiable Core Generation. Arch. Formal Proofs 2018 (2018). Accessed 2022-09-13"},{"key":"9747_CR22","unstructured":"Thiemann, R.: Duality of Linear Programming. Arch. Formal Proofs 2022 (2022). Accessed 2023-10-28"},{"key":"9747_CR23","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-29007-8_13","volume":"11715","author":"R Bottesch","year":"2019","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: Verifying an incremental theory solver for linear arithmetic in isabelle\/HOL. The 12th International Symposium on Frontiers of Combining Systems (FroCoS) 11715, 223\u2013239 (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_13","journal-title":"The 12th International Symposium on Frontiers of Combining Systems (FroCoS)"},{"key":"9747_CR24","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/S10817-013-9289-2","volume":"52","author":"E Alkassar","year":"2014","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C.: A framework for the verification of certifying computations. J. Autom. Reason. 52, 241\u2013273 (2014). https:\/\/doi.org\/10.1007\/S10817-013-9289-2","journal-title":"J. Autom. Reason."},{"key":"9747_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/BF02392606","author":"J Petersen","year":"1891","unstructured":"Petersen, J.: Die Theorie der regul\u00e4ren graphs (1891). https:\/\/doi.org\/10.1007\/BF02392606","journal-title":"Die Theorie der regul\u00e4ren graphs"},{"key":"9747_CR26","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/j.ejor.2019.09.006","volume":"291","author":"P Bir\u00f3","year":"2021","unstructured":"Bir\u00f3, P., van de Klundert, J., Manlove, D., Pettersson, W., Andersson, T., Burnapp, L., Chromy, P., Delgado, P., Dworczak, P., Haase, B., Hemke, A., Johnson, R., Klimentova, X., Kuypers, D., Nanni Costa, A., Smeulders, B., Spieksma, F., Valent\u00edn, M.O., Viana, A.: Modelling and optimisation in european kidney exchange programmes. Eur. J. Oper. Res. 291, 447\u2013456 (2021). https:\/\/doi.org\/10.1016\/j.ejor.2019.09.006","journal-title":"Eur. J. Oper. Res."},{"key":"9747_CR27","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/1284320.1284321","volume":"54","author":"A Mehta","year":"2007","unstructured":"Mehta, A., Saberi, A., Vazirani, U.V., Vazirani, V.V.: AdWords and generalized online matching. J. ACM 54, 22 (2007). https:\/\/doi.org\/10.1145\/1284320.1284321","journal-title":"J. ACM"},{"key":"9747_CR28","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1002\/nav.3800020109","volume":"2","author":"HW Kuhn","year":"1955","unstructured":"Kuhn, H.W.: The hungarian method for the assignment problem. Nav. Res. Logist. Q. 2, 83\u201397 (1955). https:\/\/doi.org\/10.1002\/nav.3800020109","journal-title":"Nav. Res. Logist. Q."},{"key":"9747_CR29","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF02579206","volume":"7","author":"K Mulmuley","year":"1987","unstructured":"Mulmuley, K., Vazirani, U.V., Vazirani, V.V.: Matching is as easy as matrix inversion. Comb. 7, 105\u2013113 (1987). https:\/\/doi.org\/10.1007\/BF02579206","journal-title":"Comb."},{"key":"9747_CR30","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0304-3975(79)90044-6","volume":"8","author":"LG Valiant","year":"1979","unstructured":"Valiant, L.G.: The complexity of computing the permanent. Theoret. Comput. Sci. 8, 189\u2013201 (1979). https:\/\/doi.org\/10.1016\/0304-3975(79)90044-6","journal-title":"Theoret. Comput. Sci."},{"key":"9747_CR31","doi-asserted-by":"publisher","first-page":"55","DOI":"10.6028\/jres.069B.013","volume":"69","author":"J Edmonds","year":"1965","unstructured":"Edmonds, J.: Maximum matching and a polyhedron with 0,1-vertices. J. Res. Natl. Bur. Stand., B Math. math. phys. 69, 55\u201356 (1965). https:\/\/doi.org\/10.6028\/jres.069B.013","journal-title":"J. Res. Natl. Bur. Stand., B Math. math. phys."},{"key":"9747_CR32","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM 14, 221\u2013227 (1971). https:\/\/doi.org\/10.1145\/362575.362577","journal-title":"Commun. ACM"},{"key":"9747_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_12","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to hopcroft\u2019s algorithm. Int. Theorem Prov. (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12","journal-title":"Int. Theorem Prov."},{"key":"9747_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_8","author":"D Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. Interactive Theorem Proving (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_8","journal-title":"Interactive Theorem Proving"},{"key":"9747_CR35","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/321941.321942","volume":"23","author":"HN Gabow","year":"1976","unstructured":"Gabow, H.N.: An efficient implementation of edmonds\u2019 algorithm for maximum matching on graphs. J. ACM 23, 221\u2013234 (1976). https:\/\/doi.org\/10.1145\/321941.321942","journal-title":"J. ACM"},{"key":"9747_CR36","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1980.12","author":"S Micali","year":"1980","unstructured":"Micali, S., Vazirani, V.V.: An $$O(\\sqrt{V}E)$$ algorithm for finding maximum matching in general graphs. 21st Annu. IEEE Symp. Found. Comput. Sci (FOCS) (1980). https:\/\/doi.org\/10.1109\/SFCS.1980.12","journal-title":"21st Annu. IEEE Symp. Found. Comput. Sci (FOCS)"},{"key":"9747_CR37","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1137\/0202019","volume":"2","author":"JE Hopcroft","year":"1973","unstructured":"Hopcroft, J.E., Karp, R.M.: An $$n^{5\/2}$$ algorithm for maximum matchings in bipartite graphs. SIAM J. Comput. 2, 225\u2013231 (1973). https:\/\/doi.org\/10.1137\/0202019","journal-title":"SIAM J. Comput."},{"key":"9747_CR38","doi-asserted-by":"publisher","first-page":"2009","DOI":"10.1287\/MOOR.2020.0388","volume":"49","author":"VV Vazirani","year":"2024","unstructured":"Vazirani, V.V.: A theory of alternating paths and blossoms from the perspective of minimum length. Math. Oper. Res. 49, 2009\u20132047 (2024). https:\/\/doi.org\/10.1287\/MOOR.2020.0388","journal-title":"Math. Oper. Res."},{"key":"9747_CR39","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1007\/BFB0032060","volume":"443","author":"N Blum","year":"1990","unstructured":"Blum, N.: A new approach to maximum matching in general graphs. the 17th international colloquium on automata. Language. Program. (ICALP) 443, 586\u2013597 (1990). https:\/\/doi.org\/10.1007\/BFB0032060","journal-title":"Language. Program. (ICALP)"},{"key":"9747_CR40","unstructured":"Vazirani, V.V.: A Theory of Alternating Paths and Blossoms for Proving Correctness of the $$O(\\sqrt{V}E)$$ General Graph Matching Algorithm. In: The 1st Integer Programming and Combinatorial Optimization Conference (IPCO), pp. 509\u2013530 (1990)"},{"key":"9747_CR41","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/BF01305952","volume":"14","author":"VV Vazirani","year":"1994","unstructured":"Vazirani, V.V.: A theory of alternating paths and blossoms for proving correctness of the $$o(\\sqrt{v} e)$$ general graph maximum matching algorithm. Combinatorica 14, 71\u2013109 (1994). https:\/\/doi.org\/10.1007\/BF01305952","journal-title":"Combinatorica"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-026-09747-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-026-09747-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-026-09747-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T10:57:27Z","timestamp":1771239447000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-026-09747-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,16]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["9747"],"URL":"https:\/\/doi.org\/10.1007\/s10817-026-09747-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,16]]},"assertion":[{"value":"2 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"2"}}