Program
Verification
Book

PV1 ⊧ RCamlchecks if a given program is type safe

Refinement type checking and inference system for OCaml

Application domain/field

Refinement type checking
Horn constraint solving
Inductive proofs
Relational specifications
Inductive theorem proving
Functional language

Type of tool

Refinement-based verifier

Expected input

OCaml program

Format:

.ml file

Expected output

Safe with a proof log/tree, or Unsafe and a counterexample/disproof.

Internals

Uses Z3.

Links

Project page: http://lfp.dip.jp/rcaml/

Related papers

Automating Induction for Solving Horn Clauses (CAV '17)

Last publication date

13 July 2017

Related tools

Automated inductive theorem techniques/tools: ACL2s, SPIKE, CLAM, IsaPlanner, Leon, Dafny, Zeno, HipSpec, CVC4.
Other Horn constraint solver: 𝜇Z (extension of Z3)

ProVerB specific

Markdown description: view/edit
Reason for this entry: CAV 2017
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.