LIPIcs.ITP.2019.18.pdf
- Filesize: 0.51 MB
- 20 pages
Document
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
Cite AsGet 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
https://doi.org/10.4230/LIPIcs.ITP.2019.18
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.
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)
0PDF Downloads