Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-02167236
Contributor : Armaël Guéneau Connect in order to contact the contributor
Submitted on : Thursday, June 27, 2019 - 3:55:29 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:07 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). Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨hal-02167236⟩

Share

Metrics

Les métriques sont temporairement indisponibles