CN is a tool for verifying that C code is free of undefined behaviour and meets user-written specifications of its ownership and functional correctness, and for translating those specifications into C assertions that can be checked at runtime on concrete test cases.
- Fulminate: Testing CN Separation-Logic Specifications in C. Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell. In POPL 2025. [ doi | pdf ]
- CN: Verifying systems C code with separation-logic refinement types. Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. In POPL 2023. [ doi | project page | pdf ]
See the tutorial documentation.
Below are the installation instructions for installing Cerberus, CN, and their dependencies.
-
Install make, git, GMP library, pkg-config and either/both Z3 or CVC5. On an Ubuntu system this is done via
sudo apt install build-essential libgmp-dev pkg-config z3Note: there is a known bug with Z3 version 4.8.13 (the default on Ubuntu 22.04) so you may wish to install Z3 via opam later for a more up-to-date version. Z3 that is provided in the docker images is sufficiently up-to-date.
-
Install the opam package manager for OCaml: https://ocaml.org/docs/installing-ocaml#install-opam. On Ubuntu,
sudo apt install opam. -
Initialise opam with a recent version of OCaml (the CI builds with 4.14.1, CN developers use 5.2.0).
opam init --yes --compiler=5.2.0 -
Clone the Cerberus repo (which includes CN):
git clone https://github.com/rems-project/cerberus.git -
For CN end users, who don't want to tinker with CN locally:
opam install --yes ./cerberus.opam ./cerberus-lib.opam ./cn.opam # z3 for a more recent version -
For CN developers:
opam install --deps-only ./cerberus.opam ./cerberus-lib.opam ./cn.opam ocamlformat.0.26.2 # one time make install_cn # after any editswhich installs Cerberus, CN (as both a library and an executable), and dependencies.
Please see our contributing guide for logistics and our onboarding guide for learning the code base.