Frama-C - Framework for Modular Analysis of C


Person in charge : MARCHÉ Claude


Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.

Frama-C gathers several static analysis techniques in a single collaborative framework. Some parts of the framework are nearing completion and can already provide useful results, while other parts should still be considered experimental. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C already provides sophisticated tools such as a slicer and dependency analysis.

More information: http://frama-c.cea.fr/

- Licence : LGPL



Research activities
  Program proof
  Formalisation and Proof of Numerical Programs
  Deductive Verification of Programs

Members
  MARCHÉ Claude
  MBIADA NDJANDA Jacques Charles

Group
  Verification of Algorithms, Languages and Systems

BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
A prototype to automate semantic mappings between taxonomies

FR1155729
Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé