×

Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. (English) Zbl 1468.68328

Summary: We present a formalization of classical algorithms for computing the maximum flow in a network: the Edmonds-Karp algorithm and the push-relabel algorithm. We prove correctness and time complexity of these algorithms. Our formal proof closely follows a standard textbook proof, and is accessible even without being an expert in Isabelle/HOL – the interactive theorem prover used for the formalization. Using stepwise refinement techniques, we instantiate the generic Ford-Fulkerson algorithm to Edmonds-Karp algorithm, and the generic push-relabel algorithm of Goldberg and Tarjan to both the relabel-to-front and the FIFO push-relabel algorithm. Further refinement then yields verified efficient implementations of the algorithms, which compare well to unverified reference implementations.

MSC:

68V20 Formalization of mathematics in connection with theorem provers
05C21 Flows in graphs
68W40 Analysis of algorithms
90C35 Programming involving graphs or networks
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Back, R.-J.: On the correctness of refinement steps in program development. Ph.D. thesis, Department of Computer Science, University of Helsinki (1978)
[2] Back, R.-J., von Wright, J.: Refinement Calculus—A Systematic Introduction. Springer, Berlin (1998) · Zbl 0949.68094 · doi:10.1007/978-1-4612-1674-2
[3] Ballarin, C.; Borwein, JM (ed.); Farmer, WM (ed.), Interpretation of locales in Isabelle (2006), Berlin
[4] Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Berlin (2010)
[5] Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Mu \[\tilde{{\text{n}}}\] n oz, C.A., Tahar, S. (eds.) TPHOL, volume 5170 of LNCS. Springer, Berlin (2008) · Zbl 1165.68352
[6] Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP. ACM, New York (2011) · Zbl 1323.68366
[7] Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Proceedings of ITP (2015) · Zbl 1465.68172
[8] Chen, R., Lévy, J.-J.: A semi-automatic proof of strong connectivity. VSTTE 2017. (2017). https://hal.inria.fr/hal-01632947 · Zbl 1403.68221
[9] Cherkassky, B.V., Goldberg, A.V.: On implementing the push—relabel method for the maximum flow problem. Algorithmica 19(4), 390-410 (1997) · Zbl 0898.68029 · doi:10.1007/PL00009180
[10] Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009) · Zbl 1187.68679
[11] Dinitz, Y.: Theoretical Computer Science. Chapter Dinitz’ Algorithm: The Original Version and Even’s Version. Springer, Berlin (2006)
[12] Edmonds, J., Karp, R.M.: Theoretical improvements in algorithmic efficiency for network flow problems. J. ACM 19(2), 248-264 (1972) · Zbl 0318.90024
[13] Filliâtre, J.-C., Paskevich, A.: Why3—Where Programs Meet Provers. Springer, Berlin (2013) · Zbl 1435.68366 · doi:10.1007/978-3-642-37036-6_8
[14] Ford, L.R., Fulkerson, D.R.: Maximal flow through a network. Can. J. Math. 8(3), 399-404 (1956) · Zbl 0073.40203 · doi:10.4153/CJM-1956-045-5
[15] Goldberg, A.V.: Andrew goldberg’s network optimization library. http://www.avglab.com/andrew/soft.html
[16] Goldberg, A.V., Tarjan, R.E.: A new approach to the maximum-flow problem. J. ACM 35(4), 921-940 (1988) · Zbl 0661.90031 · doi:10.1145/48014.61051
[17] Greenaway, D.: Automated proof-producing abstraction of C code. Ph.D. thesis, CSE, UNSW, Sydney, Australia (2015)
[18] Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: Beringer, L., Felty, A.P. (eds.) ITP. Springer, Berlin (2012) · Zbl 1360.68751
[19] Haftmann, F.: Code Generation from Specifications in Higher Order Logic. Ph.D. thesis, Technische Universität München (2009)
[20] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010, LNCS. Springer, Berlin (2010) · Zbl 1284.68131
[21] Johnson, D.S., McGeoch, C.C., et al.: Network Flows and Matching: First DIMACS Implementation Challenge. American Mathematical Society, Providence (1993) · Zbl 0781.00013 · doi:10.1090/dimacs/012
[22] Karzanov, A.V.: Determination of maximal flow in a network by method of preflows. Doklady Akademii Nauk SSSR 215(1), 49-52 (1974)
[23] Krauss, A.: Recursive definitions of monadic functions. In: Proceedings of PAR, vol. 43 (2010) · Zbl 1214.68335
[24] Lammich, P.: Refinement for monadic programs. In: Archive of Formal Proofs. http://afp.sf.net/entries/Refine_Monadic.shtml, 2012. Formal proof development (2012) · Zbl 1360.68757
[25] Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP, volume 8558 of LNCS. Springer, Berlin (2014) · Zbl 1416.68168
[26] Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP, volume 9236 of LNCS. Springer, Berlin (2015) · Zbl 1465.68290
[27] Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP. ACM, New York (2016)
[28] Lammich, P., Meis, R.: A separation logic framework for Imperative HOL. Archive of Formal Proofs, (2012). http://afp.sf.net/entries/Separation_Logic_Imperative_HOL.shtml, Formal proof development
[29] Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: Proceedings of ITP (2016) · Zbl 1468.68327
[30] Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. Archive of Formal Proofs, (2016). http://isa-afp.org/entries/EdmondsKarp_Maxflow.shtml, Formal proof development · Zbl 1468.68327
[31] Lammich, P., Sefidgar, S.R.: Flow networks and the Min-Cut-Max-Flow theorem. Archive of Formal Proofs, (June 2017). http://isa-afp.org/entries/Flow_Networks.shtml. Formal proof development
[32] Lammich, P., Sefidgar, S.R.: Formalizing push-relabel algorithms. Archive of Formal Proofs (2017). http://isa-afp.org/entries/Prpu_Maxflow.shtml, Formal proof development
[33] Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Proc. of ITP, volume 7406 of LNCS. Springer, (2012) · Zbl 1360.68757
[34] Lee, G.: Correctnesss of Ford-Fulkerson’s maximum flow algorithm. Formaliz. Math. 13(2), 305-314 (2005)
[35] Lee, G., Rudnicki, P.: Alternative aggregates in Mizar. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus ’07/MKM ’07. Springer, Berlin (2007) · Zbl 1202.68385
[36] Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 4, 3-24 (2005)
[37] MLton Standard ML compiler. http://mlton.org/
[38] Nipkow, T.: Amortized complexity verified. In: Proceedings of ITP (2015) · Zbl 1465.68059
[39] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS. Springer, Berlin (2002) · Zbl 0994.68131
[40] Nordhoff, B., Lammich, P.: Formalization of Dijkstra’s algorithm. Archive of Formal Proofs (2012). http://afp.sf.net/entries/Dijkstra_Shortest_Path.shtml, Formal proof development
[41] Noschinski, L.: Formalizing Graph Theory and Planarity Certificates. Ph.D. thesis, Fakultät für Informatik, Technische Universität München (2015) · Zbl 1308.05055
[42] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the Logic in Computer Science (LICS). IEEE (2002)
[43] Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, Boston (2011)
[44] Stanford ACM-ICPC notebook. https://github.com/jaehyunp/stanfordacm
[45] Wenzel, M.: Isar—A generic interpretative approach to readable formal proof documents. In: TPHOLs’99, volume 1690 of LNCS. Springer, Berlin (1999)
[46] Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221-227 (1971) · Zbl 0214.43005 · doi:10.1145/362575.362577
[47] Zwick, U.: The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate. Theor. Comput. Sci. 148(1), 165-170 (1995) · Zbl 0873.68159 · doi:10.1016/0304-3975(95)00022-O
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.