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.

翻译：我们提出了一种新的流框架，用于处理操作一般图程序的分离逻辑推理。该框架克服了先前发展中的问题：它基于标准不动点理论，保证最小流，排除消失流，并具有易于理解的脚印概念以满足框架规则的可靠性要求。此外，我们提出了自动化框架规则的算法，并在从并发数据结构线性化证明中提取的图更新上进行了评估。评估结果表明，我们的算法有助于自动化这些证明中的关键环节，而此前这些环节依赖于用户引导或启发式方法。