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
Erschienen in:
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

verfasst von : Arthur Charguéraud, François Pottier

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. We present a Coq formalization of this analysis. Moreover, we implement Union-Find as an OCaml library and formally endow it with a modular specification that offers a full functional correctness guarantee as well as an amortized complexity bound. Reasoning in Coq about imperative OCaml code relies on the CFML tool, which is based on characteristic formulae and Separation Logic, and which we extend with time credits. Although it was known in principle that amortized analysis can be explained in terms of time credits and that time credits can be viewed as resources in Separation Logic, we believe our work is the first practical demonstration of this approach.

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 "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

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
Vorheriges Kapitel Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
Nächstes Kapitel Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
Literatur
1.
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)MATH
2.
Alstrup, S., Thorup, M., Gørtz, I.L., Rauhe, T., Zwick, U.: Union-find with constant time deletions. ACM Trans. Algorithms 11(1), 6:1–6:28 (2014)CrossRef
3.
Amadio, rm, et al.: Certified complexity (CerCo). In: Lago, U.D., Peña, R. (eds.) FOPARA 2013. LNCS, vol. 8552, pp. 1–18. Springer, Heidelberg (2014)
4.
Atkey, R.: Amortised resource analysis with separation logic. Logical Methods in Computer Science 7(2:17), 1–33 (2011)MathSciNet
5.
Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: Functional Programming Languages and Computer Architecture (FPCA) (1995)
6.
Charguéraud, A.: Characteristic formulae for the verification of imperative programs in HOSC (2012, to appear)
7.
Charguéraud, A.: Characteristic Formulae for Mechanized Program Verification. Ph.D. Thesis, Université Paris 7 (2010)
8.
9.
Chlipala, A.: The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: International Conference on Functional Programming (ICFP) (2013)
10.
Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: International Conference on Functional Programming (ICFP) (2009)
11.
Conchon, S., Filliâtre, J.: A persistent union-find data structure. In: ACM Workshop on ML (2007)
12.
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009) MATH
13.
Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Principles of Programming Languages (POPL) (2008)
14.
Danner, N., Paykin, J., Royer, J.S.: A static cost analysis for a higher-order language. In: Programming Languages Meets Program Verification (PLPV) (2013)
15.
Galler, B.A., Fischer, M.J.: An improved equivalence algorithm. Commun. ACM 7(5), 301–303 (1964)MATHCrossRef
16.
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1–14:62 (2012)CrossRef
17.
Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287–306. Springer, Heidelberg (2010) CrossRef
18.
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Principles of Programming Languages (POPL) (2003)
19.
20.
Kaplan, H., Shafrir, N., Tarjan, R.E.: Union-find with deletions. In: Symposium on Discrete Algorithms (SODA) (2002)
21.
Kozen, D.C.: The Design and Analysis of Algorithms. Texts and Monographs in Computer Science. Springer, Heidelberg (1992)CrossRef
22.
Le Métayer, D.: ACE: an automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248–266 (1988)CrossRef
23.
Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, manuscript KRML 209 (2010)
24.
Nipkow, T.: Amortized complexity verified. In: Interactive Theorem Proving (2015)
25.
Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: Types in Language Design and Implementation (TLDI) (2011)
26.
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science (LICS) (2002)
27.
Tarjan, R.E.: Class notes: Disjoint set union (1999)
28.
Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245–281 (1984)MATHCrossRef
29.
30.
Metadaten
Titel
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
verfasst von
Arthur Charguéraud
François Pottier
Copyright-Jahr
2015
Buch
Interactive Theorem Proving

Print ISBN: 978-3-319-22101-4

Electronic ISBN: 978-3-319-22102-1

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-22102-1_9