coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Introducing Frama-C

From: Virgile Prevosto <virgile.prevosto AT m4x.org>
To: Caml list <caml-list AT yquem.inria.fr>, coq-club AT pauillac.inria.fr, why-discuss AT lists.gforge.inria.fr, frama-c-discuss AT lists.gforge.inria.fr, espass-admin-members AT lists.gforge.enseeiht.fr, Focal <focal AT modulogic.inria.fr>
Subject: [Coq-Club] Introducing Frama-C
Date: Mon, 26 May 2008 18:25:53 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Greetings.
The Frama-C development team is proud to announce the availability
of Frama-C, the framework for the development of collaborating
static analyzers for the C language. Many analyzers are provided in the
distribution, including a value analysis plug-in that provides variation
domains for the variables of the program, and Jessie, a plug-in
for computing Hoare style weakest preconditions.

Frama-C is Open Source software. It is written in Ocaml and relies
on the CIL (C Intermediate Language) library.

Additional information, source code and documentation for Frama-C
are available now at http://frama-c.cea.fr/. Binary distributions for
various popular environments will be forthcoming.

For the Frama-C development team,
--
Pascal Cuoq and Virgile Prevosto

[Coq-Club] Introducing Frama-C, Virgile Prevosto