A prototype implementation of a region and permission type system for deductive verification.

Contact: Romain Bardou


Capucine is released under the BSD license.

Latest version:

Capucine 0.3 (31/08/2011)
This is the version used in my PhD thesis. It includes the examples of the thesis.

Older versions:

Capucine 0.2 (25/10/2010)
This is the version used in the JFLA article. It includes the example of the article, as well as the Coq proof for its difficult verification condition.

Capucine 0.1 (05/10/2010)

What is Capucine?

Capucine is a prototype implementation of my PhD work. It is a language with regions, permissions and invariants for deductive verification. Regions allow some static separation of pointers, and permissions allow static tracking of the state of invariants. Capucine integrates with the Why platform: Capucine programs can be interpreted as Why programs so that Why handles generation of verification conditions for automatic provers or proof assistants.

Getting Started

This is a source distribution. To compile Capucine, you need OCaml version 3.10.2 or later (Ubuntu / Debian package: ocaml). You also need Why 2.26 to compute verification conditions, and some automatic prover such as Alt-Ergo, Simplify, Z3 or CVC3. You may also use the Coq proof assistant.

To check that Capucine compiles correctly, type:

To try out the examples, for instance to compile examples/sparse.cap and view proof obligations using GWhy, run:
make examples/sparse.gwhy

Examples (Capucine 0.3)

All these examples may also be found in the examples directory.

Examples (Capucine 0.2)

All these examples may also be found in the bench directory.


Below is a screenshot of GWhy on the finite array model (part of the Sparse Array example).