{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:59:00Z","timestamp":1781027940027,"version":"3.54.1"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vanishing flows, and has an easy to understand notion of footprint as needed for soundness of the frame rule. In addition, we present algorithms for automating the frame rule, which we evaluate on graph updates extracted from linearizability proofs for concurrent data structures. The evaluation demonstrates that our algorithms help to automate key aspects of these proofs that have previously relied on user guidance or heuristics.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_32","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"628-646","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Make Flows Small Again: Revisiting the Flow Framework"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3974-7713","authenticated-orcid":false,"given":"Sebastian","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Beki\u0107, H.: Definable operation in general algebras, and the theory of automata and flowcharts. In: Programming Languages and Their Definition. Lecture Notes in Computer Science, vol.\u00a0177, pp. 30\u201355. Springer (1984)","DOI":"10.1007\/BFb0048939"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: FSTTCS. Lecture Notes in Computer Science, vol.\u00a03328, pp. 97\u2013109. Springer (2004)","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO. Lecture Notes in Computer Science, vol.\u00a04111, pp. 115\u2013137. Springer (2005)","DOI":"10.1007\/11804192_6"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: APLAS. Lecture Notes in Computer Science, vol.\u00a03780, pp. 52\u201368. Springer (2005)","DOI":"10.1007\/11575467_5"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS. pp. 366\u2013378. IEEE (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL. pp. 289\u2013300. ACM (2009)","DOI":"10.1145\/1480881.1480917"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL. pp. 287\u2013300. ACM (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: TACAS. Lecture Notes in Computer Science, vol. 3920, pp. 287\u2013302. Springer (2006)","DOI":"10.1007\/11691372_19"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Enea, C., Leng\u00e1l, O., Sighireanu, M., Vojnar, T.: SPEN: A solver for separation logic. In: NFM. Lecture Notes in Computer Science, vol. 10227, pp. 302\u2013309 (2017)","DOI":"10.1007\/978-3-319-57288-8_22"},{"key":"32_CR10","unstructured":"Feldman, Y.M.Y., Enea, C., Morrison, A., Rinetzky, N., Shoham, S.: Order out of chaos: Proving linearizability using local views. In: DISC. LIPIcs, vol. 121, pp. 23:1\u201323:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018)"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Harris, T.L.: A pragmatic implementation of non-blocking linked-lists. In: DISC. Lecture Notes in Computer Science, vol. 2180, pp. 300\u2013314. Springer (2001)","DOI":"10.1007\/3-540-45414-4_21"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Heller, S., Herlihy, M., Luchangco, V., Moir, M., III, W.N.S., Shavit, N.: A lazy concurrent list-based set algorithm. In: OPODIS. Lecture Notes in Computer Science, vol. 3974, pp. 3\u201316. Springer (2005)","DOI":"10.1007\/11795490_3"},{"key":"32_CR13","unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: POPL. pp. 523\u2013536. ACM (2013)","DOI":"10.1145\/2429069.2429131"},{"key":"32_CR15","unstructured":"Hol\u00edk, L., Peringer, P., Rogalewicz, A., Sokov\u00e1, V., Vojnar, T., Zuleger, F.: Low-level bi-abduction. In: ECOOP. LIPIcs, vol. 222, pp. 19:1\u201319:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Hyland, J.M.E., Ong, C.L.: On full abstraction for PCF: i, ii, and III. Inf. Comput. 163(2), 285\u2013408 (2000)","DOI":"10.1006\/inco.2000.2917"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: ATVA. Lecture Notes in Computer Science, vol. 8837, pp. 201\u2013218. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, \u00a0e20 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Kam, J.B., Ullman, J.D.: Monotone data flow analysis frameworks. Acta Informatica 7, 305\u2013317 (1977)","DOI":"10.1007\/BF00290339"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Katelaan, J., Zuleger, F.: Beyond symbolic heaps: Deciding separation logic with inductive definitions. In: LPAR. EPiC Series in Computing, vol. 73, pp. 390\u2013408. EasyChair (2020)","DOI":"10.29007\/vkmj"},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: POPL. pp. 194\u2013206. ACM Press (1973)","DOI":"10.1145\/512927.512945"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Krishna, S., Patel, N., Shasha, D.E., Wies, T.: Verifying concurrent search structure templates. In: PLDI. pp. 181\u2013196. ACM (2020)","DOI":"10.1145\/3385412.3386029"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Krishna, S., Shasha, D.E., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang. 2(POPL), 37:1\u201337:31 (2018)","DOI":"10.1145\/3158125"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Krishna, S., Summers, A.J., Wies, T.: Local reasoning for global graph properties. In: ESOP. Lecture Notes in Computer Science, vol. 12075, pp. 308\u2013335. Springer (2020)","DOI":"10.1007\/978-3-030-44914-8_12"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: TACAS (1). Lecture Notes in Computer Science, vol. 10805, pp. 41\u201360. Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_3"},{"key":"32_CR26","doi-asserted-by":"publisher","unstructured":"Meyer, R., Wies, T., Wolff, S.: Artifact for \u201cA Concurrent Program Logic with a Future and History\u201d (Sep 2022). https:\/\/doi.org\/10.5281\/zenodo.7080459","DOI":"10.5281\/zenodo.7080459"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Meyer, R., Wies, T., Wolff, S.: A concurrent program logic with a future and history. Proc. ACM Program. Lang. 6(OOPSLA) (2022)","DOI":"10.1145\/3563337"},{"key":"32_CR28","doi-asserted-by":"publisher","unstructured":"Meyer, R., Wies, T., Wolff, S.: Artifact for \u201cMake flows small again: revisiting the flow framework\u201d (Jan 2023). https:\/\/doi.org\/10.5281\/zenodo.7566204","DOI":"10.5281\/zenodo.7566204"},{"key":"32_CR29","doi-asserted-by":"crossref","unstructured":"Michael, M.M.: High performance dynamic lock-free hash tables and list-based sets. In: SPAA. pp. 73\u201382. ACM (2002)","DOI":"10.1145\/564870.564881"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"Milner, R.: Fully abstract models of typed lambda-calculi. Theor. Comput. Sci. 4(1), 1\u201322 (1977)","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"32_CR31","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"32_CR32","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: CSL. Lecture Notes in Computer Science,vol.\u00a02142, pp. 1\u201319. Springer (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"32_CR33","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: PODC. pp. 85\u201394. ACM (2010)","DOI":"10.1145\/1835698.1835722"},{"key":"32_CR34","doi-asserted-by":"crossref","unstructured":"Patel, N., Krishna, S., Shasha, D.E., Wies, T.: Verifying concurrent multicopy search structures. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201332 (2021)","DOI":"10.1145\/3485490"},{"key":"32_CR35","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 773\u2013789. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"32_CR36","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 711\u2013728. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"32_CR37","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223\u2013255 (1977)","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"32_CR38","doi-asserted-by":"crossref","unstructured":"Qiu, X., Wang, Y.: A decidable logic for tree data-structures with measurements. In: VMCAI. Lecture Notes in Computer Science, vol. 11388, pp. 318\u2013341. Springer (2019)","DOI":"10.1007\/978-3-030-11245-5_15"},{"key":"32_CR39","doi-asserted-by":"crossref","unstructured":"Raad, A., Hobor, A., Villard, J., Gardner, P.: Verifying concurrent graph algorithms. In: APLAS. Lecture Notes in Computer Science, vol. 10017, pp. 314-336 (2016)","DOI":"10.1007\/978-3-319-47958-3_17"},{"key":"32_CR40","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"32_CR41","doi-asserted-by":"crossref","unstructured":"da\u00a0Rocha\u00a0Pinto, P., Dinsdale-Young, T., Gardner, P.: Tada: A logic for time and data abstraction. In: ECOOP. Lecture Notes in Computer Science, vol.\u00a08586, pp. 207\u2013231. Springer (2014)","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"32_CR42","doi-asserted-by":"crossref","unstructured":"Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: CPP. pp. 53\u201365. ACM (2017)","DOI":"10.1145\/3018610.3018623"},{"key":"32_CR43","unstructured":"Scott, D.: Outline of a mathematical theory of computation. Tech. Rep. PRG02, Oxford University Computing Laboratory (1970)"},{"key":"32_CR44","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI. pp. 77\u201387. ACM (2015)","DOI":"10.1145\/2737924.2737964"},{"key":"32_CR45","doi-asserted-by":"crossref","unstructured":"Ter-Gabrielyan, A., Summers, A.J., M\u00fcller, P.: Modular verification of heap reachability properties in separation logic. Proc. ACM Program. Lang. 3(OOPSLA), 121:1\u2013121:28 (2019)","DOI":"10.1145\/3360547"},{"key":"32_CR46","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: PLDI. pp. 125\u2013135. ACM (2008)","DOI":"10.1145\/1375581.1375598"},{"key":"32_CR47","unstructured":"Yang, H.: An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: Proceedings of the SPACE Workshop (2001)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:05:58Z","timestamp":1781024758000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}