Published February 26, 2015 | Version v1
Publication Metadata-only

Formally-Proven Kosaraju's algorithm

Théry, Laurent
Other:
Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Description

This notes explains how the Kosaraju's algorithm that computes the strong-connected components of a directed graph has been for-malised in the Coq prover using the SSReflect extension.

Additional details

Identifiers Origin repository
Created:
March 25, 2023
Modified:
November 30, 2023