2026-07-20T11:02:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11073 2024-03-06T10:47:18Z ddc:004 open_access

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm Guéneau, Armaël Jourdan, Jacques-Henri Charguéraud, Arthur Pottier, François interactive deductive program verification complexity analysis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Armaël Guéneau and Jacques-Henri Jourdan and Arthur Charguéraud and François Pottier 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.18 urn:nbn:de:0030-drops-110739 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.18 eng https://creativecommons.org/licenses/by/3.0/legalcode