A state-of-the-art formally verified incremental cycle detection algorithm

A formally verified algorithm for checking the acyclicity of a graph while incrementally adding new edges and vertices to the graph.

This particular algorithm is optimized for the case of sparse graphs.

The (amortized) complexity of m arc insertions and n vertex insertions is O(m min(m^(1/2), n^(2/3)) + n), i.e.:

• O(m sqrt(m) + n) for sparse graphs;
• O(m n^(2/3) + n) for dense graphs.

(See the companion paper for more details.)