Different breeds of Colibri live in the field

COLIBRI, Colibri2, Colibrics

COLIBRI: Ancestor tool used as a Prolog library in the model checker Gatel and in the test generation tool Pathcrawler. Since 2015 it is able to read SMT-lib files and participate in the SMT Competition.
Colibri2: Ongoing reimplementation of COLIBRI in OCaml. It features additionnaly support for quantifiers, algebraic datatypes, and algebraic numbers.
Colibrics: A formally verified constraint programming engine, aimed at embedded systems.

COLIBRI dips its beak in many flowers

Sharing information between different domains makes solving faster

Program verification requires the handling of different datastructures and types. Going from one to the others, e.g. int to floating point, is often a difficulty for SMT solvers. COLIBRI on the other hand transfers information between the different representations, so it is able to solver more practical examples.

COLIBRI is fast to the point

Using high level for floating points number allows surprising reasoning

COLIBRI handles the elements at a higher level than many other solvers. For example for each floating point number (IEEE) it keeps its possible values in an interval, and other flags such as if it is integral. It propagates this information through the formula.

$x \oplus y = 0.1 \Rightarrow x \in [-0.24999999999999997 ; 0.35 ]$

Colibri2 is learning to fly

New supported features

Colibri2 is a reimplementation of COLIBRI, the long term goal is to offer the same reasoning power that COLIBRI but with additional features:

Quantifiers and polymorphism
Algebraic datatypes
Algebraic numbers

The reasoning power for bitvectors and floating point is still lacking compared with COLIBRI.

Colibrics is by construction trustworthy

Colibrics is developed in Why3

The Colibrics is proved by construction, which allows the API to offer proved specification to the user. For example the following function adds a constraint that forces a boolean b1 to be true. The proved specification ensures that the interpretation true in the context are after the call exactly the one before the call that have also the variable b1 true.

val is_true (c:context) (b1:tb)
requires { S.mem b1 c.stb }
ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.b b1) }

The proved specification of the solve function ensures that the returned model is true in the context. If the function raise the exception Unsat, the specification ensures that no interpretation is true in the context.

val solve (c:context) : Type.model int bool
ensures { is_true_in (All.Engine.interp_of_model result) c }
ensures { Var.equal_set (All.Engine.Prob.vars c.prob) (Type.defined_model result) }
raises { Type.Unsat -> forall m. not (is_true_in m c) }