### Overview of the Colibri tools

COLIBRI
Colibri2
Colibrics

COLIBRI handles the elements at an 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.

For example for the 64bit floating-point addition: $x \oplus y = 0.1 \Rightarrow \\ x \in [-0.24999999999999997 ; 0.35 ]$

COLIBRI good for because

Example: x-y=0.1 => x \in [..;..] /\ y \in [..,..]

Colibrics proved in why3

### Start of the development of COLIBRI

COLIBRI started as a COnstraint solving LIBrary in Eclipse Prolog

### Start of the SOPRANO project

The ANR SOPRANO project allowed to gather researchers working on SMT (OcamlPro, Université Paris-Saclay) and CP (CEA, INRIA) and industrials partner (Adacore) in the domain of software verification. The goal was to merge the powerful learning of SMT and the powerful propagations of CP.

### Framework combining SMT and CP

Popop, developped during the SOPRANO project, is a framework that combined the learning of SMT and the propagation of CP. However the learning framework was to cumbersome to allow the developpement of more complicated theories than booleans and linear arithmetic.

### Development of Colibrics

Colibrics started as an experiment on the possibility to prove a simple CP solver in Why3

### Development of Colibri2

The learning developed in Popop is removed to keep only the propagation part as in COLIBRI. So the solver is named Colibri2. The first features to be available are:

• Boolean
• Linear arithmetic (using Fourier-Mostkin)
• Uninterpreted symbols
• Quantifiers

### First public release of Colibri2

The solver supports:

• Boolean
• Linear arithmetic (using Fourier-Mostkin)
• Uninterpreted symbols
• Quantifiers
• Polymorphism

In a limited way:

• Floating Point numbers
• Function ceil and floor

### Get Colibri

Colibri is only available for Desktop