Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 2/2019

01.12.2017

Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL

verfasst von: Peter Lammich, S. Reza Sefidgar

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.
Vorheriger Artikel From Types to Sets by Local Type Definition in Higher-Order Logic
Nächster Artikel Formally Verified Approximations of Definite Integrals

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
Section 10.1 provides a detailed discussion
 
2
With \(u=v\), this also implies that there are no self loops.
 
3
i. e. a path with a minimum number of edges.
 
4
I.e., \((u_0,[l_1,\ldots ,l_n],u_n)\in R^*\) iff \(\forall 0\le i < n.~(u_i,l_{i+1},u_{i+1})\in R\).
 
5
Using Cormen’s technique, we would have been able to prove a bound of \(17V^2E\).
 
6
We have not found any implementation based on relabel-to-front, and our own experiments indicate a rather poor performance.
 
7
Up to this point, the formalization models capacities as linearly ordered integral domains, which subsume reals, rationals, and integers. Thus, we could chose any executable number representation here.
 
8
Actually, the unverified reference implementations of the push–relabel algorithms [15, 44] that we use in our benchmarks (cf. Sect. 9) lack such checks, and silently report erroneous maximum flow values in case of overflow. One implementation [44] has a parser that silently ignores overflows, while the other [15] uses a too small integer type for the excess flow.
 
9
A Hoare triple is written as \({<}P{>}~c~{<}\lambda r.~Q~r{>}_t\), where P is the precondition, c the program, and Q the postcondition that also depends on the program’s return value r. Pre- and postcondition are written as separation logic assertions, where \(\text {emp}\) describes the empty heap, \(*\) is the separating conjunction, \(\uparrow \varPhi \) indicates a pure assertion, i. e. one that describes no heap content, and \(\exists _\text {A}\) is the existential quantifier lifted to assertions.
 
Literatur
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)CrossRefMATH
3.
Ballarin, C.: Interpretation of locales in Isabelle. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006, Volume 4108 of LNAI. Springer, Berlin (2006)
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}}}\)oz, C.A., Tahar, S. (eds.) TPHOL, volume 5170 of LNCS. Springer, Berlin (2008)
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)
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)
8.
9.
Cherkassky, B.V., Goldberg, A.V.: On implementing the push—relabel method for the maximum flow problem. Algorithmica 19(4), 390–410 (1997)MathSciNetCrossRefMATH
10.
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)MATH
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)MATH
13.
Filliâtre, J.-C., Paskevich, A.: Why3—Where Programs Meet Provers. Springer, Berlin (2013)CrossRef
14.
15.
16.
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)
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)
21.
Johnson, D.S., McGeoch, C.C., et al.: Network Flows and Matching: First DIMACS Implementation Challenge. American Mathematical Society, Providence (1993)CrossRefMATH
22.
Karzanov, A.V.: Determination of maximal flow in a network by method of preflows. Doklady Akademii Nauk SSSR 215(1), 49–52 (1974)MathSciNet
23.
Krauss, A.: Recursive definitions of monadic functions. In: Proceedings of PAR, vol. 43 (2010)
24.
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)
26.
Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP, volume 9236 of LNCS. Springer, Berlin (2015)
27.
Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP. ACM, New York (2016)
28.
29.
Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: Proceedings of ITP (2016)
30.
31.
32.
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)
34.
Lee, G.: Correctnesss of Ford-Fulkerson’s maximum flow algorithm. Formaliz. Math. 13(2), 305–314 (2005)MathSciNet
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)
36.
Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 4, 3–24 (2005)
37.
38.
Nipkow, T.: Amortized complexity verified. In: Proceedings of ITP (2015)
39.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS. Springer, Berlin (2002)MATH
40.
41.
Noschinski, L.: Formalizing Graph Theory and Planarity Certificates. Ph.D. thesis, Fakultät für Informatik, Technische Universität München (2015)
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.
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)CrossRefMATH
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)MathSciNetCrossRefMATH
Metadaten
Titel
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL
verfasst von
Peter Lammich
S. Reza Sefidgar
Publikationsdatum
01.12.2017
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 2/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-017-9442-4

Weitere Artikel der Ausgabe 2/2019

Journal of Automated Reasoning 2/2019 Zur Ausgabe

OriginalPaper

Formally Verified Approximations of Definite Integrals

OriginalPaper

The Flow of ODEs: Formalization of Variational Equation and Poincaré Map

OriginalPaper

Proof Pearl: Bounding Least Common Multiples with Triangles

OriginalPaper

From Types to Sets by Local Type Definition in Higher-Order Logic

OriginalPaper

Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

EditorialNotes

Selected Extended Papers of ITP 2016: Preface