A Family of Provably Correct Algorithms for Exact Triangle Counting
Matthew Andrew Lee, Tze Meng Low · 2017
In recent years, there has been renewed interest in casting graph algorithms in the language of linear algebra. By replacing the computations with appropriate operations over different semi-rings, different graph algorithms can be cast as a sequence of linear algebra operations. In this paper, we show that this recent trend allows us to leverage the Formal Linear Algebra Methods Environment (FLAME) methodology to formally specify, derive and implement a family of graph algorithms for counting the number of triangles (3-cliques) in a graph. In addition, we introduce a new back-end for the FLAME Application Programming Interface (API) that computes over sparse matrices stored in the compressed sparse row (CSR) format so that the correctness of the derived algorithm can be translated to the implementation.