Newer
Older
---
layout: post
author: Virgile Prevosto
date: 2010-09-30 12:22 +0200
categories:
title: "Welcome to the Frama-C blog"
---
[Frama-C](http://frama-c.com) 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](http://frama-c.com/acsl.html) (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](https://www.fokus.fraunhofer.de/go/device-soft_en) 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](http://rdn-consulting.com/blog/) and can be found here:
* [Part 1: the traps of C](http://rdn-consulting.com/blog/2009/05/15/guest-article-static-analysis-in-medical-device-software-part-1-the-traps-of-c/)
* [Part 2: Methodology](http://rdn-consulting.com/blog/2009/06/04/guest-article-static-analysis-in-medical-device-software-part-2-methodology/)
* [Part 3: Formal Specifications](http://rdn-consulting.com/blog/2010/03/07/guest-article-static-analysis-in-medical-device-software-part-3-formal-specifications/)