A Framework for Verifying Depth-First Search Algorithms
Peter Lammich, René Neumann · 2015
Many graph algorithms are based on depth-first search (DFS). The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.