PV6 ⊧ Cameleergenerates a proof of desired properties, can be used interactively

Deductive verifier for OCaml

Application domain/field

• Deductive verification
• Functional programming

Type of tool

Deductive verifier

Expected input

GOSPEL-annotated OCaml program. The annotations are in the form of things such as preconditions, (exceptional) postconditions and loop (in)variants.

Format:

.ml file

Expected output

It will launch the Why3 IDE from which one can use different theorem provers to discharge all proof obligations. The tool tries to translate a Why3 error back to the OCaml program if the input program is not accepted for some reason.

Internals

Cameleer takes a GOSPEL-annotated OCaml program and translates it into WhyML. Uses Why3, Alt-Ergo, CVC4, Z3 and GOSPEL.

Comments

It does not support the complete OCaml language yet. Some things that are not supported include Generalized Algebraic Data Types (GADTs) and polymorphic variants.