Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)

Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov

Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can…