Expanding CertiGraph to verify Dijkstra, Prim, and Kruskal

16 Dec 2020

Talk Recording

Access Passcode: xN8#=+es


Anshuman Mohan (Cornell)


CertiGraph [Wang et al., OOPLSA ‘19] is a Coq library for the verification of graph-manipulating C programs. In this talk, I will explain how we expanded CertiGraph to verify three classic graph traversal algorithms. Verifying Dijkstra saw us using edge-labels for the first time, and exposed an overflow bug in the standard textbook implementation. Prim required a foray into undirected graphs. Kruskal saw us calling on a previously-verified union-find, and thus required undirectedness idioms layered atop a directed graph structure. This is joint work with Wei Xiang Leow (SoC) and Aquinas Hobor (SoC and Yale-NUS).

Speaker Bio

Anshuman Mohan is a Research Assistant for Dr Aquinas Hobor. Along with other members of Dr Hobor’s team, he works on the formal verification of graph-manipulating C programs. He graduated from Yale-NUS College in 2017.