This is the dissemination page for the Cameleer tool and project. Here, one can find links to videos and online resources about the GOSPEL specification language, the Cameleer tool itself, and the ongoing verification projects.
TLDR: the main documentation about Cameleer is the CAV 2021 paper. To get a quick insight of the tool and immediately start using it, we advise you to read the CAV 20021 paper, clone the GitHub repository and play with some of the available examples.
Artifact
As a companion to the CAV 2021 paper, we submitted a complete and reusable artifact, publicly available here. This artifact is the prefered way if you want to safely reproduce our proof results and as a step-by-step guide to use Cameleer.Tutorial
We gave a three hours long tutorial during ICFP 2021. The video is publicly available here. This is mainly an hands-on introduction to the tool and the verification of OCaml programs, annotated with GOSPEL specification elements. The following five case studies are used during the tutorial:- XOR-based cipher [.ml].
- A simple applicative data structure, based on forests [.ml].
- Array scanning function, using a for-loop [.ml].
- Ephemeral implementation of a FIFO data structure [.ml].
- Leftist Heaps implementation, directly issued from the ocaml-containers library [.ml].