RCaml with Induction-based Horn Constraint Solver

This page demonstrates the induction-based Horn constraint solver proposed in the following paper:

Automating Induction for Solving Horn Clauses: Hiroshi Unno, Sho Torii, and Hiroki Sakamoto
In Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), pp.24-28 (Part II), Heidelberg, Germany, July, 2017.

The Horn constraint solver is here used as a backend of RCaml, which is an extension of the OCaml functional language with refinement type checking and inference features based on Horn constraint solving. We provide the following :

The benchmarks containing :
1. OCaml programs (mult-c.ml was fixed (2017/8/8))
2. Generated Horn constraints in SMT-LIB2 format
3. Encoding of 2. as formulas with uninterpreted functions in SMT-LIB2 format
The virtual machine and its instructions
The web interface below

Input an OCaml program and click "verify" button.

verbose mode