Formal Proof and Analysis of an Incremental Cycle Detection Algorithm: (extended version)

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-02167236
Contributor : Armaël Guéneau <>
Submitted on : Thursday, June 27, 2019 - 3:55:29 PM
Last modification on : Tuesday, July 16, 2019 - 1:22:18 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02167236, version 1

Citation

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm: (extended version). ITP 2019 - 10th Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨hal-02167236⟩

Share

Metrics

Record views

48

Files downloads

409