Formal Proof and Analysis of an Incremental Cycle Detection Algorithm - Archive ouverte HAL Access content directly
Conference Papers Year :

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

(1, 2) , (3, 4, 5) , (6) , (1, 2)
1
2
3
4
5
6

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.
Fichier principal
Vignette du fichier
main.pdf (539.21 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02167236 , version 1 (27-06-2019)

Identifiers

  • HAL Id : hal-02167236 , version 1

Cite

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⟩
209 View
349 Download

Share

Gmail Facebook Twitter LinkedIn More