MECHANIZED VERIFICATION OF GRAPH-MANIPULATING PROGRAMS

This thesis tackles the mechanized verification of realistic programs which manipulate heap-represented graphs. We construct a reusable library of formalized graph theory. It is a modular and general library for reasoning about abstract mathematical graphs. We use separation logic to define how such abstract graphs are represented concretely in the heap. To facilitate the spatial entailments involving graphs, we propose an inference rule called Localize which generalize the Ramify rule. We show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. To illustrate the generality and power of our techniques, we integrate the mathematical and spatial graph libraries into the Verified Software Toolchain and certify the functional correctness of six graph-manipulating programs written in C. Our proofs are entirely machine-checked in Coq.

Author dc:creator

• WANG SHENGYI

• Verification, Separation logic, Graph-manipulating programs, Coq, CompCert, VST