Summary of the 2010 Frama-C training session in Berlin

As part of the Device-Soft project (PICF 2009 French-German cooperation project), CEA LIST and Fraunhofer FIRST have organized a Workshop centered around Frama-C and ACSL that took place on October 21 and 22 in Berlin and was hosted by FIRST.

The workshop was a success, with around 15 participants, evenly distributed between industry and academia, and coming not only from Germany, but also from Belgium, Italy, Switzerland and United Kingdom. After a keynote by Yannick Moy, from Adacore on the evolution of the status of (formal) software verification in aeronautics standard, the program of the first day included presentation by Virgile Prevosto (CEA LIST), Jochen Burghardt (Fraunhofer FIRST) and Pascal Cuoq (CEA LIST), centered around ACSL and the usage of Frama-C's deductive verification plugin Jessie to prove that an implementation is conforming to its ACSL specification.

On the second day, Pascal Cuoq first presented the Value Analysis plugin, which uses abstract interpretation to show the absence of runtime errors in a given C program. Then, Jens Gerlach (Fraunhofer FIRST) proposed a way to use Jessie to prove that a data structure is correctly implemented, taking the example of the Stack. To conclude the workshop, Virgile Prevosto provided advice on how to drive a verification task with Frama-C, using an implementation of a sorting algorithm as an example

The presented material and source code are available below: