This repo is an ongoing attempt to verify a Binary Search Tree (BST) data structure in C, using the "Verifiable C" framework for Coq.

Build Requirements

To build this project, you'll need the Coq theorem prover and the VST library.

• See the Coq download page for instruction to download Coq: https://coq.inria.fr/download
• Software Foundations has instructions for installing VST: https://softwarefoundations.cis.upenn.edu/vc-current/Preface.html#lab3

This project is tested with Coq version 8.11 and VST version 2.6.

Project Layout

• bst.c: The C source file being verified
• bst.v: Automatically generated by CompCert. Contains the Coq AST of the bst.c source code
• bst_spec.v: Coq definitions of BSTs, their operators, and properties
• bst_holes.v: Coq definition of BSTs with a "hole". Useful in describing partial trees.
• Verif_bst.v: The main verification file. Contains the representation definitions, function specifications, and main proofs.
• my_tactics.v: Misc. tactics

Status

The proofs for search and insert are complete.

The proof for delete is a work in progress.

Misc. notes

To generate bst.v from bst.c, use clightgen:

clightgen -normalize bst.c