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. It builds on the Cerberus C semantics.
- 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 CN, and its 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 CN repo:
git clone https://github.com/rems-project/cn.git -
For CN end users, who don't want to tinker with CN locally:
opam install --yes ./cn.opam # z3 for a more recent version -
For CN developers:
opam install --deps-only ./cn.opam ocamlformat.0.27.0 # one time make install # after any editswhich installs 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.
This software has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme from grant agreement no. 101002277 "TypeFoundry", and no. 789108, ERC-AdG-2017 "ELVER"; from the UK Research and Innovation (UKRI) under the UK government’s Horizon Europe funding guarantee for ERC-AdG-2022, EP/Y035976/1 "SAFER"; from an EPSRC Doctoral Training studentship; from Google; from the Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044; and from a Royal Society University Research Fellowship URF\R1\241195 (Pulte).