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
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.