Projects / Frama-C


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. The collaborative approach allows static analyzers to build upon the results already computed by other analyzers in the framework. It provides sophisticated tools, such as a slicer and dependency analysis.

Operating Systems

RSS Recent releases

  •  04 Oct 2012 21:45

    Release Notes: This release brings improvements in the C front-end and in the value analysis (automatic context-sensitive data flow analysis), WP (verification of functional properties using Hoare logic), slicing (generation of simplified, compilable C programs), and plug-ins.

    •  10 Oct 2011 21:02

      Release Notes: This new major version includes many bugfixes and improvements. Performance improvements benefit the Value Analysis and Slicing plug-ins, the Aoraï plug-in for verification of C programs against Linear Temporal Logic formulas, the GUI, and kernel property statuses for plug-in collaboration.

      •  04 Mar 2011 21:52

      Release Notes: This release fixes bugs identified in beta version 20101202 and makes the API stable for external plug-in developers. Value analysis users, consider applying this patch before compiling: . Jessie users: this release is compatible with Why 2.29, available from . WP users: the WP plug-in will be made available separately later.

      •  05 Jan 2011 22:34

      Release Notes: Many bugfixes. Small usability improvements to the GUI. A few API changes. Value analysis: improved speed and memory consumption; handle single-precision type float as such (instead of lumping it with double as previously); better handling of structs passed as arguments to functions. A new deductive verification plug-in: WP.

      •  13 Apr 2010 13:31

        Release Notes: The support for the ACSL specification language was improved framework-wide. The value analysis benefits from numerous new options to improve precision and scale to larger codebases.

        RSS Recent comments

        04 Oct 2012 11:52 pascal_cuoq Thumbs up

        Mac OS X Mountain Lion users: please note that an OCaml compiler bug affects the ability to run OCaml programs on Mountain Lion. This includes Frama-C:


        Project Spotlight


        A Java framework for building data integration and ETL applications.


        Project Spotlight

        Caché Monitor

        A dev utility for the InterSystems database Caché.