A Family of Provably Correct Algorithms for Exact
Triangle Counting
Author/Presenters
Event Type
Workshop
Applications
Correctness
Debugging
Reliability
SIGHPC Workshop
Verification
TimeSunday, November 12th11:04am -
11:21am
Location501
DescriptionIn 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.
Author/Presenters




