We present formalisations of the correctness of executable algorithms to solve minimum-cost flow problems in Isabelle/HOL. Two of the algorithms are based on the technique of scaling, most notably Orlin's algorithm, which has the fastest known running time for solving the problem of minimum-cost flow. We also include a formalisation of the worst-case running time argument for Orlin's algorithm. Our verified implementation of this algorithm, which is derived by the technique of stepwise refinement, is fully executable and was integrated into a reusable formal library on graph algorithms. Because the problems for which Orlin's algorithm works are restricted, we also verified an executable reduction from the general minimum-cost flow problem. We believe we are the first to formally consider the problem of minimum-cost flows and, more generally, any scaling algorithms. Our work has also led to a number of mathematical insights and improvements to proofs as well as theorem statements, compared to all existing expositions.

翻译：我们在Isabelle/HOL中形式化验证了求解最小成本流问题的可执行算法的正确性。其中两种算法基于缩放技术，特别是Orlin算法——该算法在求解最小成本流问题时具有已知最快的运行时间。我们还形式化验证了Orlin算法最坏情况运行时间的论证。通过逐步精化技术推导出的该算法验证实现完全可执行，并已集成至可复用的图算法形式化库中。由于Orlin算法适用的问题类型受限，我们还验证了从通用最小成本流问题出发的可执行规约方法。我们相信这是首次对最小成本流问题——更广义而言，对任何缩放算法——进行形式化研究。与现有所有论述相比，我们的工作还衍生出若干数学洞见，并改进了证明过程及定理表述。