A Family of Provably Correct Algorithms for Exact Triangle Counting
Workshop: 1st International Workshop on Software Correctness for HPC Applications (Correctness 2017)
Authors: Tze Meng Low (Carnegie Mellon University)
Abstract: 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.
Workshop Index