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

Merge branch 'colibri-doc' into 'colibri'

Colibri doc, publication and posts

See merge request !2
parents 07316639 a76dc6ae
Pipeline #38390 passed with stage
in 51 seconds
- 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
---
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
---
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ï."
---
---
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
---
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
---
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
---
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
---
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
---
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.
---
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.
---
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.
---
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."
---
---
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
---
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."
---
---
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."
---
---
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
---
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
---
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
---
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
---
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.
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