CapucineA prototype implementation of a region and permission type system for deductive verification.Contact: Romain Bardou |
Capucine is released under the BSD license.
Capucine 0.3 (31/08/2011)
This is the version used in my PhD thesis. It includes the examples
of the thesis.
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 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.
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:
make
make examples/sparse.gwhy
All these examples may also be found in the examples directory.
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).
