ICE-based Refinement Type Discovery for Higher-Order Functional Programs

<div>This dataset contains the code and benchmarks needed to replicate the experimental results presented in the TACAS 2016 paper "ICE-based Refinement Type Discovery for Higher-Order Functional Programs".</div><div><br></div><div>The verification of higher-order functional programs is a challenging problem, the existing approaches to which are hampered by the need for predicates describing loops and components behave in order for verification to be possible. Here, a novel approach intended to overcome these requirements by combining the existing refinement types approach with the invariant discovery framework ICE is presented.</div><div><br></div><div>This novel implementation consists of two parts. First, a front end written in OCaml, named RType (https://github.com/hopv/r_type), that generates Horn clauses from programs written in a subset of OCaml (as described in section 2 of the accompanying paper). Second, a Horn clause solver written in Rust, named HoIce (https://github.com/hopv/hoice), that implements the modified ICE framework presented in the accompanying paper.</div><div><br></div><div>The novel implementation as well as the benchmarks and scripts needed to reproduce its evaluation are presented here. Further details on those benchmarks and instructions on running them can be found in the <b>README</b> file.