TY - GEN
T1 - Make Flows Small Again
T2 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023
AU - Meyer, Roland
AU - Wies, Thomas
AU - Wolff, Sebastian
N1 - Publisher Copyright:
© 2023, The Author(s).
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - Frame Inference
KW - Graph Algorithms
KW - Separation Logic
UR - http://www.scopus.com/inward/record.url?scp=85161382681&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85161382681&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-30823-9_32
DO - 10.1007/978-3-031-30823-9_32
M3 - Conference contribution
AN - SCOPUS:85161382681
SN - 9783031308222
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 628
EP - 646
BT - Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
A2 - Sankaranarayanan, Sriram
A2 - Sharygina, Natasha
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 22 April 2023 through 27 April 2023
ER -