{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:53:18Z","timestamp":1758707598265,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"vor","delay-in-days":13,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005713","name":"Technische Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005713","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents a detailed verification of the Gale-Shapley algorithm for stable matching (or marriage). The verification proceeds by stepwise transformation of programs and proofs. The initial steps are on the level of imperative programs, ending in a linear time algorithm. An executable functional program is obtained in a last step. The emphasis is on the stepwise development of the algorithm and the required invariants.<\/jats:p>","DOI":"10.1007\/s10817-024-09700-x","type":"journal-article","created":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T18:02:46Z","timestamp":1718388166000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Gale-Shapley Verified"],"prefix":"10.1007","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0730-515X","authenticated-orcid":false,"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,14]]},"reference":[{"issue":"1","key":"9700_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1017\/S0956796812000019","volume":"22","author":"K Aehlig","year":"2012","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. J. Funct. Program. 22(1), 9\u201330 (2012)","journal-title":"J. Funct. Program."},{"key":"9700_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Texts in Computer Science","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. In: Texts in Computer Science. Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-1-84882-745-5"},{"key":"9700_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Texts and Monographs in Computer Science","author":"KR Apt","year":"1991","unstructured":"Apt, K.R., Olderog, E.: Verification of Sequential and Concurrent Programs. In: Texts and Monographs in Computer Science. Springer, New York (1991). https:\/\/doi.org\/10.1007\/978-1-4757-4376-0"},{"issue":"7","key":"9700_CR4","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1145\/359545.359566","volume":"21","author":"HG Baker","year":"1978","unstructured":"Baker, H.G.: Shallow binding in LISP 1.5. Commun. ACM 21(7), 565\u2013569 (1978). https:\/\/doi.org\/10.1145\/359545.359566","journal-title":"Commun. ACM"},{"issue":"8","key":"9700_CR5","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/122598.122614","volume":"26","author":"HG Baker","year":"1991","unstructured":"Baker, H.G.: Shallow binding makes functional arrays fast. ACM SIGPLAN Notices 26(8), 145\u2013147 (1991). https:\/\/doi.org\/10.1145\/122598.122614","journal-title":"ACM SIGPLAN Notices"},{"key":"9700_CR6","unstructured":"Bijlsma, A.: Formal derivation of a stable marriage algorithm. In: Feijen, W., van Gastreren, A. (eds.) C.S. Scholten dedicata: van oude machines en nieuwe rekenwijzen. Academic Service Schoonhoven (1991). https:\/\/dspace.library.uu.nl\/handle\/1874\/19385. Accessed 22 May 2024"},{"key":"9700_CR7","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Hoboken (1976)"},{"issue":"1","key":"9700_CR8","doi-asserted-by":"publisher","first-page":"9","DOI":"10.2307\/2312726","volume":"69","author":"D Gale","year":"1962","unstructured":"Gale, D., Shapley, L.S.: College admissions and the stability of marriage. Am. Math. Mon. 69(1), 9\u201315 (1962). https:\/\/doi.org\/10.2307\/2312726","journal-title":"Am. Math. Mon."},{"key":"9700_CR9","unstructured":"Gammie, P.: Stable matching. Archive of Formal Proofs (2016). Formal proof development. https:\/\/isa-afp.org\/entries\/Stable_Matching.html. Accessed 22 May 2024"},{"key":"9700_CR10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"MC Gordon","year":"1989","unstructured":"Gordon, M.C.: Mechanizing programming logics in higher order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving. Springer, New York (1989)"},{"key":"9700_CR11","series-title":"Foundations of computing series","volume-title":"The Stable marriage problem\u2014structure and algorithms","author":"D Gusfield","year":"1989","unstructured":"Gusfield, D., Irving, R.W.: The Stable marriage problem\u2014structure and algorithms. Foundations of computing series, MIT Press, Cambridge (1989)"},{"key":"9700_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming, 10th International Symposium, FLOPS 2010","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, 10th International Symposium, FLOPS 2010. Lecture Notes in Computer Science, vol. 6009, pp. 103\u2013117. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"key":"9700_CR13","doi-asserted-by":"publisher","unstructured":"Hamid, N.A., Castleberry, C.: Formally certified stable marriages. In: Proceedings of the 48th Annual Southeast Regional Conference, ACM SE \u201910. ACM (2010). https:\/\/doi.org\/10.1145\/1900008.1900056","DOI":"10.1145\/1900008.1900056"},{"key":"9700_CR14","volume-title":"Algorithm Design","author":"J Kleinberg","year":"2006","unstructured":"Kleinberg, J., Tardos, E.: Algorithm Design. Addison-Wesley, Boston (2006)"},{"key":"9700_CR15","volume-title":"Mariages Stables et leurs relations avec d\u2019autres probl\u00e8mes combinatoires","author":"DE Knuth","year":"1976","unstructured":"Knuth, D.E.: Mariages Stables et leurs relations avec d\u2019autres probl\u00e8mes combinatoires. Les Presses de l\u2019Universit\u00e9 de Montr\u00e9al, Montreal (1976)"},{"key":"9700_CR16","doi-asserted-by":"crossref","unstructured":"Knuth, D.E.: Stable Marriage and its Relation to Other Combinatorial Problems. American Mathematical Society (1997). Translation of [15]","DOI":"10.1090\/crmp\/010"},{"key":"9700_CR17","unstructured":"Lammich, P.: Collections framework. Archive of Formal Proofs (2009). Formal proof development. https:\/\/isa-afp.org\/entries\/Collections.html. Accessed 22 May 2024"},{"key":"9700_CR18","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Refinement to imperative\/hol. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving\u20146th International Conference, ITP 2015, LNCS, vol. 9236, pp. 253\u2013269. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"9700_CR19","doi-asserted-by":"publisher","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, LNCS, vol. 6172, pp. 339\u2013354. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_24","DOI":"10.1007\/978-3-642-14052-5_24"},{"issue":"3","key":"9700_CR20","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/2805789.2805800","volume":"45","author":"BM Maggs","year":"2015","unstructured":"Maggs, B.M., Sitaraman, R.K.: Algorithmic nuggets in content delivery. SIGCOMM Comput. Commun. Rev. 45(3), 52\u201366 (2015). https:\/\/doi.org\/10.1145\/2805789.2805800","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"9700_CR21","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction\u2014CADE-19, LNCS","author":"F Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) Automated Deduction\u2014CADE-19, LNCS, vol. 2741, pp. 121\u2013135. Springer, Berlin (2003)"},{"key":"9700_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-642-22863-6_21","volume-title":"Interactive Theorem Proving, ITP 2011","author":"T Nipkow","year":"2011","unstructured":"Nipkow, T.: Verified efficient enumeration of plane graphs modulo isomorphism. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving, ITP 2011. Lecture Notes in Computer Science, vol. 6898, pp. 281\u2013296. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_21"},{"key":"9700_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Gale-Shapley algorithm. Archive of Formal Proofs (2021). Formal proof development. https:\/\/isa-afp.org\/entries\/Gale_Shapley.html. Accessed 22 May 2024","DOI":"10.1007\/s10817-024-09700-x"},{"key":"9700_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics with Isabelle\/HOL. Springer (2014). http:\/\/concrete-semantics.org. Accessed 22 May 2024","DOI":"10.1007\/978-3-319-10542-0"},{"key":"9700_CR25","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"9700_CR26","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics, TPHOLs\u201999, LNCS","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Thery, L. (eds.) Theorem Proving in Higher Order Logics, TPHOLs\u201999, LNCS, vol. 1690, pp. 167\u2013183. Springer, Berlin (1999)"},{"key":"9700_CR27","unstructured":"Wenzel, M.: Isabelle\/isar\u2014a versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002). http:\/\/nbn-resolving.de\/urn\/resolver.pl?urn:nbn:de:bvb:91-diss2002020117092"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09700-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09700-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09700-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,22]],"date-time":"2024-06-22T07:08:11Z","timestamp":1719040091000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09700-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9700"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09700-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,6]]},"assertion":[{"value":"13 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 April 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2024","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":"Conflict of interest"}}],"article-number":"12"}}