Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Armaël Guéneau (1, 2) , Jacques-Henri Jourdan (3, 4, 5) , Arthur Charguéraud (6) , François Pottier (1, 2)

1 GALLIUM - Langages de programmation, types, compilation et preuves
2 CAMBIUM - Langages de programmation : systèmes de types, concurrence, preuve de programme
3 LRI - Laboratoire de Recherche en Informatique
4 CNRS - Centre National de la Recherche Scientifique
5 VALS - LRI - Vérification d'Algorithmes, Langages et Systèmes (LRI)
6 CAMUS - Compilation pour les Architectures MUlti-coeurS

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.

Mots clés: Complexity analysis; Interactive deductive program verification

Domaines: Langage de programmation [cs.PL]

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⟩