Welcome to the Frama-C blog
Virgile Prevosto - 30th Sep 2010Frama-C is an extensible platform dedicated to the analysis of C programs. It provides various plug-ins for navigating in a C code and better understanding its semantics. It can also be used to guarantee the absence of run-time error in a given program. At last, given a specification expressed in ACSL (ANSI/ISO C Specification Language), it is possible with Frama-C to prove formally that an implementation meets this specification.
This blog, started as part of the Device-Soft project will give you some examples of tasks that can be performed with Frama-C and ACSL. Articles will be written both by Frama-C developers and Frama-C users and will concentrate on the usage of the tool.
A first set of three articles explaining how static analysis can be used to analyse software present in embedded systems is hosted by RDN Consulting and can be found here: