A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.