Frama-C 2013 - Tutorial: Specification and Proof of Programs with Frama-C

Organisers:
Nikolai Kosmatov, Software Safety Laboratory, CEA LIST, France
Virgile Prevosto, Software Safety Laboratory, CEA LIST, France
Julien Signoles, Software Safety Laboratory, CEA LIST, France
Despite the spectacular progress made by the developers of formal verification tools, their usage remains basically reserved for the most critical software. More and more engineers and researchers today are interested in such tools in order to integrate them into their everyday work. This half-day tutorial proposes a practical introduction during which the participants will write C program specifications, observe the proof results, analyze proof failures and fix them. Participants will be taught how to write a specification for a C program, in the form of function contracts, and easily prove it with an automatic tool in FRAMA-C, a freely available software verification toolset. Those who will have FRAMA-C and JESSIE installed (e.g. from ready-to-install packages frama-c, why, alt-ergo under Linux) will also run automatic proof of programs on their computer. Program specifications will be written in the specification language ACSL similar to other specification languages like JML that some participants may know. ACSL-syntax is intentionally close to C and can be easily learned on-the-fly.
The tutorial is aimed mainly at software engineering students and professionals who will learn more about the state of the art in automated software verification and how it could help them in their career in software development or validation. Using freely available tools FRAMA-C and JESSIE will allow them to quickly install and try the tools. Software engineering lecturers will also be interested in how a tool such as FRAMA-C can help in teaching software verification. The only necessary background is some familiarity with the C language.