QUICr is a library for construcing abstract domains for sets of numbers from abstract domains for numbers.

QUICr is supplied as an example analyzer for a language of sets and numbers. This analyzer is provided with three numeric domains: octagons, polyhedra, and equivalence classes.


QUICr library depends on Z3 packaged for OCaml. We provide an ocamlfind compatible package for Z3..

QUICr is not currently provided as an ocamlfind package. It is intended to be included in individual projects directly. However, to aid that process, QUICr itself can be included by copying the src/quicr directory and the src/QUICr.mlpack files to your project. These depend on the z3 and num packages being specified in

The example analyzer also requires a current install of APRON.

Once these dependencies are installed, simply typing make should compile a useable version of the example analyzer.

Tour and Documentation

The documentation is not yet complete, but some documentation and examples are provided on the website.