DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2019.18

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

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

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{gueneau_et_al:LIPIcs.ITP.2019.18,
  author =	{Gu\'{e}neau, Arma\"{e}l and Jourdan, Jacques-Henri and Chargu\'{e}raud, Arthur and Pottier, Fran\c{c}ois},
  title =	{{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.18},
  URN =		{urn:nbn:de:0030-drops-110739},
  doi =		{10.4230/LIPIcs.ITP.2019.18},
  annote =	{Keywords: interactive deductive program verification, complexity analysis}
}

Search Results

Documents authored by Charguéraud, Arthur

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Abstract

Cite as

Thanks for your feedback!

Could not send message