Commit bf57cbdc authored by François Bobot's avatar François Bobot
Browse files

Start the COLIBRI manual in the website

      Allows to link publications directly and highlight them
parent a76dc6ae
Pipeline #38490 passed with stages
in 8 minutes and 11 seconds
......@@ -57,6 +57,7 @@ link: URL to access to the publication <-- optional
year: year of publication
category: "<kind of publication>"
short: "A short description for the publication." <-- optional
citeid: "Used for linking with #citeid" <-- optional
---
Abstract of the publication <-- optional (but highly recommended)
```
......@@ -95,4 +96,4 @@ If you want to generate specific HTML pages for your publication (for example
online exercices for a publication in the `teaching` category), proceed as
above, but in the `html` directory instead of `download`. See for example
the directory: `html/publications/2010-ensiie-vslg` and its corresponding
publication file `_fc-publications/general/2010-ensiie-vslg`.
\ No newline at end of file
publication file `_fc-publications/general/2010-ensiie-vslg`.
......@@ -4,6 +4,7 @@ authors: "Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin"
title: "Sharpening Constraint Programming approaches for Bit-Vector Theory"
link: "https://hal-cea.archives-ouvertes.fr/cea-01795779"
category: foundational
citeid: "CPAIOR2017"
---
Abstract : We address the challenge of developing efficient Constraint
......
......@@ -3,6 +3,7 @@ plugin: "colibri"
authors: "François Bobot, Zakaria Chihani and Bruno Marre"
title: "Real Behavior of Floating Point"
link: "https://hal.archives-ouvertes.fr/cea-01795760"
citeid: "SMT2017"
category: foundational
---
......
......@@ -2,7 +2,7 @@
plugin: "colibri"
authors: "Bruno Marre, François Bobot"
title: "COLIBRI manual"
link: "http://frama-c.com/download/frama-c-wp-manual.pdf"
link: "/html/colibri_manual.html"
category: manuals
short: "The official manual for COLIBRI."
---
......@@ -10,7 +10,10 @@
{% for pub in publis reversed %}
{% assign content = pub.content | strip_newlines %}
<details {% if content == "" %} class="empty" {% endif %}>
<details
{% if content == "" %} class="empty" {% endif %}
{% if pub.citeid %}id="{{ pub.citeid }}"{% endif %}
>
<summary tabindex="0">
{% if pub.authors %}<div>{{ pub.authors }}</div>{% endif %}
<div><b>{{ pub.title }}</b>{% if pub.link %} [<a href="{{ pub.link }}">link</a>] {% endif %}</div>
......@@ -25,4 +28,4 @@
{% endfor %}
{% endif %}
\ No newline at end of file
{% endif %}
......@@ -64,6 +64,10 @@ details.empty:hover,details.empty summary,details.empty summary:hover {
background-color: transparent!important;
}
details:target {
background-color: #ffa;
}
summary {
/* forces summary to cover the details zone,
so that it is entirely clickable.
......@@ -245,4 +249,4 @@ details[open].empty summary::before,details.empty summary::before {
padding-top: 65px;
background: white;
z-index: 3;
}
\ No newline at end of file
}
---
layout: doc_page
title: COLIBRI manual
description: COLIBRI manual
---
## COLIBRI manual ##
COLIBRI is a library
(COnstraint LIBrary for ve-RI-fi-cation) developed at
CEA LIST and used for verification or test data generation purposes
since 2000, using the techniques of constraint programming.
The variety of types and constraints provided by COLIBRI makes it possible to
use it in many testing tools at CEA LIST like GATeL [gatelMBT10], for model based
testing from Lustre/SCADE, and Osmose [BardinH08],
for structural testing from binary code, PathCrawler tool for
concolic C testing.
COLIBRI is a finite domain solver that use usual constraint
programming techniques. The basis is that one or many domains are
attached to each terms, and the constraints tighten the domains of one
term using the domains of the other terms involve in the constraint.
When no constraints could improve anymore the domain of any term, a
decision is made. Usually it splits the domain in two, but other
techniques can be used as 3B filtering which decide on the extremes of
the domains and if unsatisfiable try to improve this bound.
The domains are very specific, no reduction to simpler theory like
bit-blasting is used. COLIBRI uses a domain of union of intervals for
real and integer inter-reduced with a domain of congruence. For
floating points it uses a domain of intervals. For bit-vector a domain
that indicates if the bits are set, unset or unknown.
In addition to these domains which reason on local properties, COLIBRI
uses for integer, reals, and floating point DBM. The DBM use lots of
patterns to be able to do limited but useful non-linear reasoning.
The power of the reasoning of COLIBRI, in particular in the floating
point, are due to the information sharing and inter dependencies of all these
reasoning techniques.
The combination of all the components of COLIBRI is simplified since,
like all CP-solver, all the domains and constraints are improving the
same model.
COLIBRI gained in previous year the ability to handle SMTLIB2 format
(*QF_FP*, and *QF_BVFP* theory), but since
historically it handled only simple and double format with nearest to
even rounding([SMT2017](/html/publications.html#SMT2017),[CPAIOR2017](/html/publications.html#CPAIOR2017)), the
reasoning for other rounding mode is minimal (except in useful case
like truncation, ceiling, ...), and other formats are not supported.
# SMTLIB format ##
COLIBRI can read the SMTLIB format using [Dolmen](https://github.com/Gbury/dolmen)
......@@ -23,7 +23,7 @@ description: Quick access to the documentation of Frama-C and the plugins develo
<h4 class="tileTitle"><span>COLIBRI</span></h4>
<ul>
<li><a href="/html/kernel.html">Description page</a></li>
<li><a href="/download/frama-c-user-manual.pdf">User manual</a></li>
<li><a href="/html/colibri_manual.html">User manual</a></li>
<li><a href="https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md">Installation</a></li>
<li><a href="/html/get-frama-c.html">Releases</a></li>
<!-- <li><a href="/html/publications.html">List of publications</a></li> -->
......
......@@ -48,7 +48,7 @@ css: publications
<div class="wrap">
<h1 class="pageTitle">Publications</h1>
<h1 id="general" class="anchor"> Frama-C Framework </h1>
<h1 id="general" class="anchor"> Colibri tools </h1>
{% include publication-entries.html
title="Manuals" category="manuals" plugin="general" %}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment