CertiGraph

A library for verifying graph-manipulating programs.

Powered by Coq and VST. Compatible with CompCert.

The OVERVIEW describes what it's for, and the demo gives a brief tutorial introduction.

This version of CertiGraph is compatible with Coq 8.13 (and probably 8.14), CompCert 3.9, and VST 2.8.

Contributors

• Aquinas Hobor
• Shengyi Wang
• Anshuman Mohan

Papers

• Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms (CAV 2021). Aquinas Hobor, Anshuman Mohan, Wei Xiang Leow.
• Mechanized verification of graph-manipulating programs (Thesis). Shengyi Wang.
• A Machine-Checked C Implementation of Dijkstra's Shortest Path Algorithm. Aquinas Hobor, Anshuman Mohan, Shengyi Wang.
• Certifying Graph-Manipulating C Programs via Localizations within Data Structures (OOPSLA 2019). Aquinas Hobor, Shengyi Wang, Qinxiang Cao, Anshuman Mohan.

Installing

The library can be installed using opam. Different packages are offered for different target architectures. You can install multiple targets side-by-side.

x86_64-linux

$ opam install ./coq-certigraph.opam

x86_32-linux

$ opam install ./coq-certigraph-32.opam

Building without installing

It is possible to build CertiGraph without installing it as a library. This is useful if you simply want to check out the examples or if you want to hack on CertiGraph itself.

x86_64-linux

First, make sure you have all of the dependencies.

1. This can be done via opam:

$ opam install --deps-only ./coq-certigraph.opam

2. Alternatively, you can fetch and compile the dependencies by hand. In that case, be sure to edit the CONFIGURE file to specify the path to CompCert and/or VST.

3. Or, if your Coq Platform install includes CompCert and VST, then you may already have all the needed libraries.

Once the dependencies are in place you can perform the build:

$ make clean
$ make depend
$ make -j4

x86_32-linux

First, make sure you have all of the dependencies.

1. This can be done via opam:

$ opam install --deps-only ./coq-certigraph-32.opam

2. Alternatively, you can fetch and compile the dependencies by hand. In that case, be sure to edit the CONFIGURE file to specify the path to CompCert and/or VST.

3. Or, if your Coq Platform install includes CompCert and VST, then you may already have all the needed libraries.

Once the dependencies are in place you can perform the build:

$ make BITSIZE=32 clean
$ make BITSIZE=32 depend
$ make BITSIZE=32 -j4

Developing within CertiGraph

1. Add your C source and clightgen output to the CertiGraph directory:
   1. Write your newfile.c inside CertiGraph.
   2. path_to_clightgen/clightgen -DCOMPCERT -normalize -isystem . newfile.c
   3. Add newfile.v to the list of sources in Makefile
   4. make depend (this is for every time you edit the makefile)
   5. make path_to_newfile/newfile.vo (note the .vo)
2. Create the file verif_newfile.v. Now something like Require Import CertiGraph.path.to.newfile. will go through inside verif_newfile.v.