Document Open Access Logo

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Authors Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

Thumbnail PDF


  • Filesize: 0.51 MB
  • 20 pages

Document Identifiers

Author Details

Armaël Guéneau
  • Inria, Paris, France
Jacques-Henri Jourdan
  • CNRS, LRI, Univ. Paris Sud, Université Paris Saclay, France
Arthur Charguéraud
  • Inria & Université de Strasbourg, CNRS, ICube, Strasbourg, France
François Pottier
  • Inria, Paris, France

Cite AsGet BibTex

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 18:1-18:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Graph algorithms analysis
  • Theory of computation → Program verification
  • Software and its engineering → Correctness
  • Software and its engineering → Software performance
  • interactive deductive program verification
  • complexity analysis


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail