{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T09:08:56Z","timestamp":1747386536486,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,1,15]],"date-time":"2022-01-15T00:00:00Z","timestamp":1642204800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,15]],"date-time":"2022-01-15T00:00:00Z","timestamp":1642204800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["153217"],"award-info":[{"award-number":["153217"]}],"id":[{"id":"10.13039\/501100001711","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":[[2022,11]]},"DOI":"10.1007\/s10817-022-09616-4","type":"journal-article","created":{"date-parts":[[2022,1,15]],"date-time":"2022-01-15T10:02:48Z","timestamp":1642240968000},"page":"585-610","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5851-494X","authenticated-orcid":false,"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,15]]},"reference":[{"key":"9616_CR1","doi-asserted-by":"publisher","unstructured":"Aharoni, R.: Menger\u2019s theorem for graphs containing no infinite paths. Eur. J. Comb. 4, 201\u2013204 (1983). https:\/\/doi.org\/10.1016\/S0195-6698(83)80012-2","DOI":"10.1016\/S0195-6698(83)80012-2"},{"key":"9616_CR2","doi-asserted-by":"publisher","unstructured":"Aharoni, R., Berger, E.: Menger\u2019s theorem for infinite graphs. Invent. Math. 176(1), 1\u201362 (2009). https:\/\/doi.org\/10.1007\/s00222-008-0157-3","DOI":"10.1007\/s00222-008-0157-3"},{"key":"9616_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jctb.2010.08.002","volume":"101","author":"R Aharoni","year":"2010","unstructured":"Aharoni, R., Berger, E., Georgakopoulos, A., Perlstein, A., Spr\u00fcssel, P.: The max-flow min-cut theorem for countable networks. J. Combinat. Theory, Ser. B 101, 1\u201317 (2010). https:\/\/doi.org\/10.1016\/j.jctb.2010.08.002","journal-title":"J. Combinat. Theory, Ser. B"},{"key":"9616_CR4","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74, 568\u2013589 (2009). https:\/\/doi.org\/10.1016\/j.scico.2007.09.002","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"9616_CR5","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1006\/jcss.1999.1683","volume":"60","author":"C Baier","year":"2000","unstructured":"Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187\u2013231 (2000). https:\/\/doi.org\/10.1006\/jcss.1999.1683","journal-title":"J. Comput. Syst. Sci."},{"key":"9616_CR6","doi-asserted-by":"publisher","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani F. (Eds.) TYPES 2003, LNCS, vol. 3085, pp. 34\u201350. Springer (2004). doi: https:\/\/doi.org\/10.1007\/978-3-540-24849-13","DOI":"10.1007\/978-3-540-24849-13"},{"key":"9616_CR7","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":"9616_CR8","doi-asserted-by":"publisher","first-page":"1093","DOI":"10.1007\/s10817-019-09537-9","volume":"64","author":"C Ballarin","year":"2020","unstructured":"Ballarin, C.: Exploring the structure of an algebra text with locales. J. Autom. Reason. 64, 1093\u20131121 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09537-9","journal-title":"J. Autom. Reason."},{"key":"9616_CR9","doi-asserted-by":"publisher","unstructured":"Barthe, G., Espitau, T., Hsu, J., Sato, T., Strub, P.Y.: *-liftings for differential privacy. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl A. (Eds.) ICALP 2017, LIPIcs, vol.\u00a080, pp. 102:1\u2013102:12. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2017). doi: https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.102","DOI":"10.4230\/LIPIcs.ICALP.2017.102"},{"key":"9616_CR10","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella\u00a0B\u00e9guelin, S.: Formal Certification of Code-based Cryptographic Proofs. In: POPL 2009, pp. 90\u2013101. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"9616_CR11","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: ITP 2014, LNCS, vol. 8558, pp. 93\u2013110. Springer (2014). doi: https:\/\/doi.org\/10.1007\/978-3-319-08970-67","DOI":"10.1007\/978-3-319-08970-67"},{"issue":"6","key":"9616_CR12","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/BF02036949","volume":"2","author":"N Bourbaki","year":"1949","unstructured":"Bourbaki, N.: Sur le th\u00e9or\u00e8me de Zorn. Arch. Math. 2(6), 434\u2013437 (1949)","journal-title":"Arch. Math."},{"key":"9616_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45198-4","volume-title":"Semantics of Probabilistic Processes","author":"Y Deng","year":"2014","unstructured":"Deng, Y.: Semantics of Probabilistic Processes. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-662-45198-4"},{"key":"9616_CR14","unstructured":"Desharnais, J.: Labelled Markov Processes. Ph.D. Thesis, McGill University (1999)"},{"issue":"2","key":"9616_CR15","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1145\/321694.321699","volume":"19","author":"J Edmonds","year":"1972","unstructured":"Edmonds, J., Karp, R.M.: Theoretical improvements in algorithmic efficiency for network flow problems. J. ACM 19(2), 248\u2013264 (1972). https:\/\/doi.org\/10.1145\/321694.321699","journal-title":"J. ACM"},{"key":"9616_CR16","doi-asserted-by":"publisher","first-page":"399","DOI":"10.4153\/CJM-1956-045-5","volume":"8","author":"LR Ford","year":"1956","unstructured":"Ford, L.R., Fulkerson, D.R.: Maximal flow through a network. Can. J. Math. 8, 399\u2013404 (1956). https:\/\/doi.org\/10.4153\/CJM-1956-045-5","journal-title":"Can. J. Math."},{"key":"9616_CR17","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang X. (Eds.) ITP 2015, LNCS, vol. 9236, pp. 203\u2013220. Springer (2015). doi: https:\/\/doi.org\/10.1007\/978-3-319-22102-113","DOI":"10.1007\/978-3-319-22102-113"},{"key":"9616_CR18","doi-asserted-by":"publisher","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and Transfer: A modular design for quotients in Isabelle\/HOL. In: CPP 2013, LNCS, vol. 8307, pp. 131\u2013146. Springer (2013). doi: https:\/\/doi.org\/10.1007\/978-3-319-03545-19","DOI":"10.1007\/978-3-319-03545-19"},{"key":"9616_CR19","unstructured":"Immler, F.: Generic construction of probability spaces for paths of stochastic processes in Isabelle\/HOL. Master\u2019s thesis, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"9616_CR20","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/BF01470505","volume":"144","author":"HG Kellerer","year":"1961","unstructured":"Kellerer, H.G.: Funktionen auf Produktr\u00e4umen mit vorgegebenen Marginal-Funktionen. Math. Ann. 144, 323\u2013344 (1961). https:\/\/doi.org\/10.1007\/BF01470505","journal-title":"Math. Ann."},{"key":"9616_CR21","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10817-018-9464-6","volume":"62","author":"O Kun\u010dar","year":"2019","unstructured":"Kun\u010dar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62, 237\u2013260 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9464-6","journal-title":"J. Autom. Reason."},{"key":"9616_CR22","doi-asserted-by":"publisher","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: J.C. Blanchette, S.\u00a0Merz (eds.) ITP 2016, LNCS, vol. 9807, pp. 219\u2013234. Springer (2016). doi: https:\/\/doi.org\/10.1007\/978-3-319-43144-414","DOI":"10.1007\/978-3-319-43144-414"},{"key":"9616_CR23","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":"9616_CR24","unstructured":"Lee, G.: Correctnesss of Ford-Fulkerson\u2019s maximum flow algorithm. Formal. Math. 13(2), 305\u2013314 (2005). https:\/\/fm.mizar.org\/2005-13\/pdf13-2\/glib_005.pdf"},{"key":"9616_CR25","unstructured":"Lochbihler, A.: A formal proof of the max-flow min-cut theorem for countable networks. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/MFMC_Countable.shtml, Formal proof development"},{"key":"9616_CR26","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher-order logic. In: P.\u00a0Thiemann (ed.) ESOP 2016, LNCS, vol. 9632, pp. 503\u2013531. Springer (2016). doi: https:\/\/doi.org\/10.1007\/978-3-662-49498-120","DOI":"10.1007\/978-3-662-49498-120"},{"key":"9616_CR27","unstructured":"Lochbihler, A.: Probabilistic while loop. Archive of Formal Proofs (2017). https:\/\/isa-afp.org\/entries\/Probabilistic_While.html, Formal proof development"},{"key":"9616_CR28","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: A mechanized proof of the max-flow min-cut theorem for countable networks. In: Cohen, L., Kaliszyk C. (Eds.) ITP 2021, LIPIcs, vol. 193, pp. 25:1\u201325:18 (2021). doi: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.25","DOI":"10.4230\/LIPIcs.ITP.2021.25"},{"key":"9616_CR29","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. http:\/\/www.andreas-lochbihler.de\/pub\/lochbihler-mfmc.pdf (2021)","DOI":"10.1007\/s10817-022-09616-4"},{"key":"9616_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/9781316672815","volume-title":"Probability on Trees and Networks","author":"R Lyons","year":"2017","unstructured":"Lyons, R., Peres, Y.: Probability on Trees and Networks. Cambridge University Press, New York (2017). https:\/\/doi.org\/10.1017\/9781316672815"},{"key":"9616_CR31","doi-asserted-by":"publisher","unstructured":"Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Grundy, J., Newey M. (Eds.) TPHOLs 1998, LNCS, vol. 1479, pp. 349\u2013366. Springer (1998). doi: https:\/\/doi.org\/10.1007\/BFb0055146","DOI":"10.1007\/BFb0055146"},{"key":"9616_CR32","doi-asserted-by":"publisher","unstructured":"Sabot, C., Tournier, L.: Random walks in Dirichlet environment: an overview. Annales de la Facult\u00e9 des sciences de Toulouse: Math\u00e9matiques Ser. 6, 26(2), 463\u2013509 (2017). doi: https:\/\/doi.org\/10.5802\/afst.1542","DOI":"10.5802\/afst.1542"},{"key":"9616_CR33","doi-asserted-by":"publisher","unstructured":"Sack, J., Zhang, L.: A general framework for probabilistic characterizing formulae. In: Kuncak, V., Rybalchenko, A. (Eds.) VMCAI 2012, LNCS, vol. 7148, pp. 396\u2013411. Springer (2012). doi: https:\/\/doi.org\/10.1007\/978-3-642-27940-926","DOI":"10.1007\/978-3-642-27940-926"},{"key":"9616_CR34","doi-asserted-by":"publisher","unstructured":"Smolka, G., Sch\u00e4fer, S., Doczkal, C.: Transfinite constructions in classical type theory. In: Urban, C., Zhang, X., (Eds.) ITP 2015, LNCS, vol. 9236, pp. 391\u2013404. Springer (2015). doi: https:\/\/doi.org\/10.1007\/978-3-319-22102-126","DOI":"10.1007\/978-3-319-22102-126"},{"issue":"2","key":"9616_CR35","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1214\/aoms\/1177700153","volume":"36","author":"V Strassen","year":"1965","unstructured":"Strassen, V.: The existence of probability measures with given marginals. Ann. Math. Stat. 36(2), 423\u2013439 (1965). https:\/\/doi.org\/10.1214\/aoms\/1177700153","journal-title":"Ann. Math. Stat."},{"key":"9616_CR36","unstructured":"Wiedijk, F.: The de Bruijn factor. https:\/\/www.cs.ru.nl\/~freek\/factor\/factor.pdf (2000)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09616-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09616-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09616-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T11:12:17Z","timestamp":1667646737000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09616-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,15]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9616"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09616-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,1,15]]},"assertion":[{"value":"21 August 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 January 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}