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:
- Experience Report: "Formal Verification in Aeronautics: Current Practise and Upcoming Standard": Yannick Moy (Adacore) [slides]
- Introduction to ACSL and its GUI: Virgile Prevosto (CEA LIST) [slides| source code]
- Basic ACSL features, Exercise: simple-loop program inspecting an array: Jochen Burghardt (Fraunhofer FIRST) [slides| source code]
- Advanced ACSL features, Predicate definitions, Exercise: simple-loop program modifying an array: Pascal Cuoq (CEA LIST) [source code]
- Short presentation of Value Analysis and its use of ACSL: Pascal Cuoq (CEA LIST) [source code]
- Deductive verification of data structures: Jens Gerlach (Fraunhofer FIRST) [slides| source code]
- Tips and tricks in verification: Virgile Prevosto (CEA LIST) [slides| source code]