Formal Proof and Analysis of an Incremental Cycle Detection Algorithm


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.


Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier
ITP: International Conference on Interactive Theorem Proving, September 2019