Remove Frama-C publications and add colibri one

_data/publications.yml

 - id: public
-  name: Plug-ins distributed with Frama-C
-  short: Distributed plug-ins
+  name: Colibri open-source tools
+  short: Open source tools
   plugins:
-  - id: eva
-    name: Eva, an Evolved Value Analysis
-    short: Eva
-  - id: wp
-    name: WP
-  - id: e-acsl
-    name: E-ACSL
-  - id: aorai
-    name: Aoraï
-  - id: slicing
-    name: Security slicing
-    short: Slicing
-- id: internal
-  name: Internal plug-ins at CEA
-  short: Internal plug-ins
-  plugins:
-  - id: cfp
-    name: CFP
-  - id: ltest
-    name: LTest
-  - id: metacsl
-    name: MetACSL
-  - id: pathcrawler
-    name: PathCrawler
-  - id: rpp
-    name: RPP
-  - id: secureflow
-    name: SecureFlow
-- id: external
-  name: External plug-ins
-  plugins:
-  - id: c2s
-    name: Conc2Seq
-  - id: celia
-    name: CELIA
-  - id: cost
-    name: Cost
-  - id: fanc
-    name: Fan-C
-  - id: jessie
-    name: Jessie
-  - id: sante
-    name: SANTE
-  - id: sidan
-    name: SIDAN
-  - id: stac
-    name: STAC
-  - id: stady
-    name: StaDy
-  - id: taster
-    name: Taster
\ No newline at end of file
+  - id: colibri
+    name: COLIBRI
+  - id: colibri2
+    name: Colibri2
+  - id: colibrics
+    name: Colibrics

_fc-publications/aorai/2009-afadl-gs.md

----
-plugin: "aorai"
-authors: "Julien Groslambert and Nicolas Stouls"
-title: "Vérification de propriétés LTL sur des programmes C par génération d'annotations"
-book: "Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)"
-link: http://hal.archives-ouvertes.fr/inria-00568947
-year: 2009
-category: foundational
-short: "In French."
----
-
-Ce travail propose une méthode de vérification de propriétés temporelles basée sur la génération automatique d'annotations de programmes. Les annotations générées sont ensuite vérifiées par des prouveurs automatiques via un calcul de plus faible précondition. Notre contribution vise à optimiser une technique existante de génération d'annotations, afin d'améliorer l'automatisation de la vérification des obligations de preuve produites. Cette approche a été outillée sous la forme d'un plugin au sein de l'outil Frama-C pour la vérification de programmes C.
\ No newline at end of file

_fc-publications/aorai/user-manual.md

----
-plugin: "aorai"
-authors: "Nicolas Stouls"
-title: "Aoraï Plug-in Tutorial"
-link: "http://frama-c.com/download/aorai/aorai-manual.pdf"
-category: manuals
-short: "The official manual of the Frama-C plug-in Aoraï."
----

_fc-publications/c2s/2016-scam-bkll.md

----
-plugin: "c2s"
-authors: "Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre and Frédéric Loulergue"
-title: "Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs"
-book: "16th International Working Conference on Source Code Analysis and Manipulation (SCAM)"
-link: https://hal.archives-ouvertes.fr/hal-01423641/en
-year: 2016
-category: foundational
----
-
-Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers. 
\ No newline at end of file

_fc-publications/c2s/2017-lifo-blk.md

----
-plugin: "c2s"
-authors: "Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue"
-title: "Concurrent Program Verification by Code Transformation: Correctness"
-book: "LIFO Research Report RR-2017-03"
-link: https://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2017/RR-2017-03.pdf
-year: 2017
-category: other
-short: "Complete version of \"From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation\""
----
-
-Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq.
\ No newline at end of file

_fc-publications/c2s/2017-vpt-blk.md

----
-plugin: "c2s"
-authors: "Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue"
-title: "From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation"
-book: "Fifth International Workshop on Verification and Program Transformation (VPT)"
-link: https://hal.archives-ouvertes.fr/hal-01495454/en
-year: 2017
-category: foundational
----
-
-Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed conc2seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind conc2seq, and present an effort towards the full mechanization of both the for- malization and proofs with the proof assistant Coq. 
\ No newline at end of file

_fc-publications/celia/2011-pldi-bdes.md

----
-plugin: "celia"
-authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighireanu"
-title: "On inter-procedural analysis of programs with lists and data"
-book: "Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI)"
-link: https://www.di.ens.fr/~cezarad/pldi11.pdf
-year: 2011
-category: foundational
----
-
-We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. Program configurations are represented by graphs where nodes represent list segments without sharing. The data in these list segments are characterized by constraints in abstract domains. We consider a domain where constraints are in a universally quantified fragment of the first-order logic over sequences, as well as a domain constraining the multisets of data in sequences.
-
-Our analysis computes the effect of each procedure in a local manner, by considering only the reachable part of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domain.
-
-The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking.
\ No newline at end of file

_fc-publications/celia/2012-vmcai-bdes.md

----
-plugin: "celia"
-authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighireanu"
-title: "Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data"
-book: "International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI)"
-link: https://www.irif.fr/~cenea/papers/vmcai2012-lists.pdf
-year: 2012
-category: foundational
----
-
-We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs.
\ No newline at end of file

_fc-publications/cfp/2017-lopstr-as.md

----
-plugin: "cfp"
-authors: "Michele Alberti and Julien Signoles"
-title: "Context Generation from Formal Specifications for C Analysis Tools"
-book: "Logic-based Program Synthesis and Transformation (LOPSTR)"
-link: http://julien.signoles.free.fr/publis/2017_lopstr.pdf
-year: 2017
-category: foundational
-short: "Best paper award."
----
-
-Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. This may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible.
-
-This paper presents a way to systematically generate such a context from a formal specification of a C function. This is applied to a subset of the ACSL specification language in order to generate suitable contexts for the abstract interpretation-based value analysis plug-ins of Frama-C, a framework for analysis of code written in C. The idea here presented has been implemented in a new Frama-C plug-in which is currently in use in an operational industrial setting. 
-

_fc-publications/colibri/bitvector_cpaior2017.md

+---
+plugin: "colibri"
+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
+---
+
+Abstract : We address the challenge of developing efficient Constraint
+Programming-based approaches for solving formulas over the quantifier-free
+fragment of the theory of bitvectors (BV), which is of paramount importance in
+software verification. We propose CP(BV), a highly efficient BV resolution
+technique built on carefully chosen anterior results sharpened with key original
+features such as thorough domain combination or dedicated labeling. Extensive
+experimental evaluations demonstrate that CP(BV) is much more efficient than
+previous similar attempts from the CP community, that it is indeed able to solve
+the majority of the standard verification benchmarks for bitvectors, and that it
+already complements the standard SMT approaches on several crucial (and
+industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width,
+theory combination or intricate mix of non-linear arithmetic and bitwise
+operators. This work paves the way toward building competitive CP-based
+verification-oriented solvers.

_fc-publications/colibri/float_smt2017.md

+---
+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"
+category: foundational
+---
+
+Abstract : We present an efficient constraint programming (CP) approach to the
+SMTLIB theory of quantifier-free floating-point arithmetic (QF FP). We rely on
+dense interreduction between many domain representations to greatly reduce the
+search space. We compare our tool to current state-of-the-art SMT solvers and
+show that it is consistently better on large problems involving non-linear
+arithmetic operations (for which bit-blasting techniques tend to scale badly).
+Our results emphasize the importance of the conservation of the high-level
+structure of the original problems.

_fc-publications/wp/user-manual.md → _fc-publications/colibri/user-manual.md

 ---
-plugin: "wp"
-authors: "Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, Allan Blanchard"
-title: "WP Plug-in Manual"
+plugin: "colibri"
+authors: "Bruno Marre, François Bobot"
+title: "COLIBRI manual"
 link: "http://frama-c.com/download/frama-c-wp-manual.pdf"
 category: manuals
-short: "The official manual for the WP plug-in."
+short: "The official manual for COLIBRI."
 ---

_fc-publications/colibri2/smt2018.md

+---
+plugin: "colibri2"
+authors: "François Bobot, Stéphane Graham-Lengrand, Bruno Marre, Guillaume Bury "
+title: "Centralizing equality reasoning in MCSAT"
+link: "https://hal.archives-ouvertes.fr/hal-01935591"
+category: foundational
+---
+
+Abstract : MCSAT is an approach to SMT-solving that uses assignments of values
+to first-order variables in order to try and build a model of the input formula.
+When different theories are combined, as formalized in the CDSAT system,
+equalities between variables and terms play an important role, each theory
+module being required to understand equalities and which values are equal to
+which. This paper broaches the topic of how to reason about equalities in a
+centralized way, so that the theory reasoners can avoid replicating equality
+reasoning steps, and even benefit from a centralized implementation of
+equivalence classes of terms, which is based on a equality graph (Egraph). This
+paper sketches the design of a prototype based on this architecture.
+
+The current version of Colibri2 doesn't use learning anymore, it hindered the
+addition of new theories and reasonings

_fc-publications/colibri2/user-manual.md

+---
+plugin: "colibri2"
+authors: "François Bobot"
+title: "Colibri2 manual"
+link: "http://frama-c.com/download/frama-c-wp-manual.pdf"
+category: manuals
+short: "The official manual for Colibri2."
+---

_fc-publications/colibrics/user-manual.md

+---
+plugin: "colibrics"
+authors: "François Bobot"
+title: "Colibrics manual"
+link: "http://frama-c.com/download/frama-c-wp-manual.pdf"
+category: manuals
+short: "The official manual for Colibrics."
+---

_fc-publications/cost/2012-fmics-amarg.md

----
-plugin: "cost"
-authors: "Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas"
-title: "Certifying and reasoning on cost annotations in C programs"
-book: "Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)"
-link: http://hal.inria.fr/hal-00702665/en
-year: 2012
-category: foundational
----
-
-We present a so-called labelling method to enrich a compiler in order to turn it into a "cost annotating compiler", that is, a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. The first contribution of this paper is a proof methodology that extends standard simulation proofs of compiler correctness to ensure that the cost annotations on the source code are sound and precise with respect to an execution cost model of the object code. As a second contribution, we demonstrate that our label-based instrumentation is scalable because it consists in a modular extension of the compilation chain. To that end, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in OCaml for (a large fragment of) the C language. As a third and last contribution, we provide evidence for the usability of the generated cost annotations as a mean to reason on the concrete complexity of programs written in C. For this purpose, we present a Frama-C plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the C language. These logic assertions are synthetic in the sense that they characterize the cost of executing the entire program, not only constant-time fragments. (These bounds may depend on the size of the input data.) We report our experimentations on some C programs, especially programs generated by a compiler for the synchronous programming language Lustre used in critical embedded software. 
\ No newline at end of file

_fc-publications/e-acsl/2013-rv-kps.md

----
-plugin: "e-acsl"
-authors: "Nikolai Kosmatov, Guillaume Petiot and Julien Signoles"
-title: "An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs"
-book: "Proceedings of Runtime Verification (RV)"
-link: https://hal.archives-ouvertes.fr/cea-01834990/en
-year: 2013
-category: other
----
-
-Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. However, monitoring of annotations for pointers and memory locations (such as being valid, initialized, in a particular block, with a particular offset, etc.) is not straightforward and requires systematic instrumentation and monitoring of memory-related operations. This paper describes the runtime memory monitoring library we developed for execution support of E-ACSL, executable specification language for C programs offered by the Frama-C platform for analysis of C code. We present the global architecture of our solution as well as various optimizations we realized to make memory monitoring more efficient. Our experiments confirm the benefits of these optimizations and illustrate the bug detection potential of runtime assertion checking with E-ACSL. 
\ No newline at end of file

_fc-publications/e-acsl/2013-rv-ks.md

----
-plugin: "e-acsl"
-authors: "Nikolai Kosmatov and Julien Signoles"
-title: "A Lesson on Runtime Assertion Checking with Frama-C"
-book: "International Conference on Runtime Verification (RV)"
-link: "http://julien.signoles.free.fr/publis/2013_rv.pdf"
-year: 2013
-category: tutorials
-short: "A tutorial about the Frama-C plug-in E-ACSL."
----
-
-Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language E-ACSL and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.
\ No newline at end of file

_fc-publications/e-acsl/2013-sac-dks.md

----
-plugin: "e-acsl"
-authors: "Michaël Delahaye, Nikolai Kosmatov and Julien Signoles"
-title: "Common Specification Language for Static and Dynamic Analysis of C Programs"
-book: "Proceedings of Symposium on Applied Computing (SAC)"
-link: https://hal.inria.fr/hal-00853721/en
-year: 2013
-category: foundational
-short: "An overview of the specification language."
----
-
-Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents e-acsl, subset of the acsl specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.
\ No newline at end of file

_fc-publications/e-acsl/2015-jfla-jks.md

----
-plugin: "e-acsl"
-authors: "Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles"
-title: "Rester statique pour devenir plus rapide, plus précis et plus mince"
-book: "Journées Francophones des Langages Applicatifs (JFLA)"
-link: http://julien.signoles.free.fr/publis/2015_jfla.pdf
-year: 2015
-category: other
-short: "In French"
----
-
-E-ACSL est un greffon de Frama-C, une plateforme d'analyse de codes C qui est
-développée en OCaml. Son but est de transformer un programme C formellement
-annoté dans le langage de spécification éponyme E-ACSL en un autre programme C
-dont le comportement à l'exécution est équivalent si toutes les spécifications
-sont dynamiquement vérifiées et qui échoue sur la première spécification
-fausse sinon. Pour cela, une instrumentation du programme source est notamment
-effectuée afin, d'une part, de conserver les informations nécessaires à
-l'évaluation des prédicats E-ACSL et, d'autre part, de traduire correctement
-ces derniers.
-
-Cet article présente deux analyses statiques qui améliorent grandement la
-précision de cette transformation de programmes en réduisant l'instrumentation
-effectuée. Ainsi, le code généré est plus rapide et consomme moins de mémoire
-lors de son exécution. La première analyse est un système de types fondé sur
-une inférence d'intervalles et permettant de distinguer les entiers
-(mathématiques) pouvant être convertis en des expressions C de type "entier
-machine" de ceux devant être traduits vers des entiers en précision
-arbitraire. La seconde analyse est une analyse flot de données arrière
-sur-approximante paramétrée par une analyse d'alias. Elle permet de limiter
-l'instrumentation des opérations sur la mémoire à celles ayant un impact
-potentiel sur la validité d'une annotation formelle.