Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach

What is it about?

It was thought to be hard to mathematically prove that programs that manipulate graphs in computer memory using pointers do their work correctly. We show that by thinking about the graphs as having a specific mathematical structure, we can more easily combine and rearrange their parts in a proof, making it simpler to write. We give two new correctness proofs of classic graph programs in this style: one that explores each node of a graph while using minimal extra memory, and another that uses graphs to implement a data structure to efficiently organize and fetch related items.

Featured Image

Photo by GuerrillaBuzz on Unsplash

Photo by GuerrillaBuzz on Unsplash

Why is it important?

The traditional method of proving pointer-manipulating programs correct, known as "separation logic", has its main strength in allowing you to reason "locally" by focusing on relevant parts of memory — essentially only paying attention to the data that your program accesses. This is a very powerful concept, called "framing", but it usually only works at the surface level of a proof. Using our mathematical framework, we extend this foundational aspect of separation logic so that it can be applied at different conceptual levels throughout the proofs, making them more modular.