Document Open Access Logo

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Authors Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2019.18.pdf
  • Filesize: 0.51 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Graph algorithms analysis
  • Theory of computation → Program verification
  • Software and its engineering → Correctness
  • Software and its engineering → Software performance
Keywords
  • interactive deductive program verification
  • complexity analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized asymptotic complexity of the modified algorithm.

Cite As Get BibTex

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.18

Author Details

Armaël Guéneau
  • Inria, Paris, France
Jacques-Henri Jourdan
  • CNRS, LRI, Univ. Paris Sud, Université Paris Saclay, France
Arthur Charguéraud
  • Inria & Université de Strasbourg, CNRS, ICube, Strasbourg, France
François Pottier
  • Inria, Paris, France

Supplementary Materials

References

  1. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. Journal of Formalized Reasoning, 11(1):43-76, 2018. Google Scholar
  2. Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, and Damiano Zanardini. Cost analysis of object-oriented bytecode programs. Theoretical Computer Science, 413(1):142-159, 2012. Google Scholar
  3. Robert Atkey. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7(2:17), 2011. Google Scholar
  4. Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, and Robert E. Tarjan. A New Approach to Incremental Cycle Detection and Related Problems. ACM Transactions on Algorithms, 12(2):14:1-14:22, 2016. Google Scholar
  5. Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, and Zhong Shao. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verification (CAV), volume 10427 of Lecture Notes in Computer Science, pages 64-85. Springer, 2017. Google Scholar
  6. Arthur Charguéraud. Characteristic Formulae for the Verification of Imperative Programs, 2013. Unpublished. URL: http://www.chargueraud.org/research/2013/cf/cf.pdf.
  7. Arthur Charguéraud. The CFML tool and library. http://www.chargueraud.org/softs/cfml/, 2019.
  8. Arthur Charguéraud and François Pottier. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. Journal of Automated Reasoning, 2017. Google Scholar
  9. Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Algorithm in Why3, Coq, and Isabelle. Manuscript, 2018. Google Scholar
  10. Ran Chen and Jean-Jacques Lévy. A Semi-automatic Proof of Strong Connectivity. In Verified Software: Theories, Tools and Experiments, volume 10712 of Lecture Notes in Computer Science, pages 49-65. Springer, 2017. Google Scholar
  11. Nils Anders Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Principles of Programming Languages (POPL), 2008. Google Scholar
  12. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. In Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pages 463-478. Springer, 2013. Google Scholar
  13. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning, 58(1):3-31, 2017. Google Scholar
  14. Sumit Gulwani. SPEED: symbolic complexity bound analysis. In Computer Aided Verification (CAV), volume 5643 of Lecture Notes in Computer Science, pages 51-62. Springer, 2009. Google Scholar
  15. Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. SPEED: precise and efficient static estimation of program computational complexity. In Principles of Programming Languages (POPL), pages 127-139, 2009. Google Scholar
  16. Armaël Guéneau. Dune pull request #1955, March 2019. Google Scholar
  17. Armaël Guéneau, Arthur Charguéraud, and François Pottier. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In European Symposium on Programming (ESOP), volume 10801 of Lecture Notes in Computer Science, pages 533-560. Springer, 2018. Google Scholar
  18. Maximilian P. L. Haslbeck and Tobias Nipkow. Hoare Logics for Time Bounds: A Study in Meta Theory. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 10805 of Lecture Notes in Computer Science, pages 155-171. Springer, 2018. Google Scholar
  19. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. Google Scholar
  20. Jan Hoffmann, Ankush Das, and Shu-Chun Weng. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL), pages 359-373, 2017. Google Scholar
  21. Benjamin Holland, Ganesh Ram Santhanam, Payas Awadhutkar, and Suresh Kothari. Statically-Informed Dynamic Analysis Tools to Detect Algorithmic Complexity Vulnerabilities. In Source Code Analysis and Manipulation (SCAM), pages 79-84, 2016. Google Scholar
  22. John E. Hopcroft. Computer Science: The Emergence of a Discipline. Communications of the ACM, 30(3):198-202, 1987. Google Scholar
  23. Jacques-Henri Jourdan. Coq pull request #89, July 2015. Google Scholar
  24. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. Google Scholar
  25. Peter Lammich. Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm. In Interactive Theorem Proving (ITP), volume 8558 of Lecture Notes in Computer Science, pages 325-340. Springer, 2014. Google Scholar
  26. Peter Lammich. Refinement to Imperative/HOL. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 253-269. Springer, 2015. Google Scholar
  27. Peter Lammich and René Neumann. A Framework for Verifying Depth-First Search Algorithms. In Certified Programs and Proofs (CPP), pages 137-146, 2015. Google Scholar
  28. Caroline Lemieux, Rohan Padhye, Koushik Sen, and Dawn Song. PerfFuzz: Automatically generating pathological inputs. In International Symposium on Software Testing and Analysis (ISSTA), pages 254-265, 2018. Google Scholar
  29. Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. Contract-based resource verification for higher-order functions with memoization. In Principles of Programming Languages (POPL), pages 330-343, 2017. Google Scholar
  30. Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, and Robert Bruce Findler. A Coq Library for Internal Verification of Running-Times. In Functional and Logic Programming, volume 9613 of Lecture Notes in Computer Science, pages 144-162. Springer, 2016. Google Scholar
  31. Rashmi Mudduluru and Murali Krishna Ramanathan. Efficient Flow Profiling for Detecting Performance Bugs. In International Symposium on Software Testing and Analysis (ISSTA), pages 413-424, 2016. Google Scholar
  32. Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. In Luis Caires, editor, European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 1-27. Springer, 2019. Google Scholar
  33. Tobias Nipkow. Amortized Complexity Verified. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 310-324. Springer, 2015. Google Scholar
  34. Oswaldo Olivo, Isil Dillig, and Calvin Lin. Static detection of asymptotic performance bugs in collection traversals. In Programming Language Design and Implementation (PLDI), pages 369-378, 2015. Google Scholar
  35. Matthew Parkinson and Gavin Bierman. Separation logic and abstraction. In Principles of Programming Languages (POPL), pages 247-258, 2005. Google Scholar
  36. François Pottier. Depth-First Search and Strong Connectivity in Coq. In Journées Françaises des Langages Applicatifs (JFLA), 2015. Google Scholar
  37. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS), pages 55-74, 2002. Google Scholar
  38. David M. Russinoff. A Mechanically Verified Incremental Garbage Collector. Formal Aspects of Computing, 6(4):359-390, 1994. URL: https://doi.org/10.1007/BF01211305.
  39. Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq. In Interactive Theorem Proving (ITP), volume 8558 of Lecture Notes in Computer Science, pages 499-514. Springer, 2014. Google Scholar
  40. Akhilesh Srikanth, Burak Sahin, and William R. Harris. Complexity verification using guided theorem enumeration. In Principles of Programming Languages (POPL), pages 639-652, 2017. Google Scholar
  41. Jane Street. Dune: A composable build system, 2018. Google Scholar
  42. Robert Endre Tarjan. Amortized Computational Complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306-318, 1985. Google Scholar
  43. Robert Endre Tarjan. Algorithmic Design. Communications of the ACM, 30(3):204-212, 1987. Google Scholar
  44. The Coq development team. The Coq Proof Assistant, 2019. Google Scholar
  45. Luca Della Toffola, Michael Pradel, and Thomas R. Gross. Synthesizing programs that expose performance bottlenecks. In Code Generation and Optimization (CGO), pages 314-326, 2018. Google Scholar
  46. Eelis van der Weegen and James McKinna. A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. In Types for Proofs and Programs, volume 5497 of Lecture Notes in Computer Science, pages 256-271. Springer, 2008. Google Scholar
  47. Ben Wegbreit. Mechanical Program Analysis. Communications of the ACM, 18(9):528-539, 1975. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact