Tutorials

Frama-C Framework

Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue
A Lesson on Verification of IoT Software with Frama-C [link]
In International Conference on High Performance Computing & Simulation (HPCS), 2019

This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things.

Nikolai Kosmatov and Julien Signoles
Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis [link]
In International Conference on Runtime Verification (RV), 2016

Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language, ACSL.

This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs

Virgile Prevosto
Frama-C tutorial
In STANCE Project, 2013
David Mentré
Practical introduction to Frama-C [link]
In Mitsubishi Electric R&D Centre Europe, 2013

Examples

WP

Allan Blanchard
Introduction to C Program Proof with Frama-C and its WP plug-in [link]
A comprehensive tutorial on how to prove C programs with Frama-C and WP.
Jens Gerlach, Denis Efremov and Tim Sikatzki
ACSL by Example [link]
A fairly complete tour of ACSL and WP features through various functions inspired from C++ STL.

GitHub repository

Virgile Prevosto
Frama-C WP tutorial [link]
In Laboratoire d'Informatique Fondamentale d'Orléans, 2014
A tutorial about the Frama-C plug-in WP.

LIFO’s website

Annotated files

Virgile Prevosto, Nikolay Kosmatov and Julien Signoles
Specification and Proof of Programs with Frama-C [link]
In Integrated Formal Methods (iFM), 2013
A tutorial about the Frama-C plug-in WP.

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 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.

Annotated files

E-ACSL

Nikolai Kosmatov and Julien Signoles
A Lesson on Runtime Assertion Checking with Frama-C [link]
In International Conference on Runtime Verification (RV), 2013
A tutorial about the Frama-C plug-in E-ACSL.

Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language E-ACSL and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.

PathCrawler

Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro
A Lesson on Structural Testing with PathCrawler-online.com [link]
In International Conference on Tests and Proofs (TAP), 2012

PathCrawler is a test generation tool developed at CEA LIST for structural testing of C programs. The new version of PathCrawler is developed in an entirely novel form: that of a test-case generation web service which is freely accessible at PathCrawler-online.com. This service allows many test-case generation sessions to be run in parallel in a completely robust and secure way. This tool demo and teaching experience paper presents PathCrawler-online.com in the form of a lesson on structural software testing, showing its benefits, limitations and illustrating the usage of the tool on simple examples.

Nicky Williams and Nikolai Kosmatov
Structural Testing with PathCrawler. Tutorial Synopsis [link]
In International Conference on Quality Software (QSIC), 2012

Automatic testing tools allow huge savings but they do not exonerate the user from thinking carefully about what they want testing to achieve. To successfully use the Path Crawler-online structural testing tool, the user must provide not only the full source code, but also must set the test parameters and program the oracle. This demands a different”mindset” from that used for informal functional-style manual testing, as we explain with the help of several examples.

Jessie

Nikolai Kosmatov, Virgile Prevosto and Julien Signoles
A Lesson on Proof of Programs with Frama-C [link]
In International Conference on Runtime Verification (RV), 2013

Recent advances on proof of programs based on deductive methods allow verification tools to be successfully integrated into industrial verification processes. However, their usage remains mostly confined to the verification of the most critical software. One of the obstacles to their deeper penetration into industry is the lack of engineers properly trained in formal methods. A wider use of formal verification methods and tools in industrial verification requires their wider teaching and practical training for software engineering students as well as professionals.

This tutorial paper presents a lesson on proof of programs in the form of several exercises followed by their solutions. It is based on our experience in teaching at several French universities over the last four years. This experience shows that, for the majority of students, theoretical courses (like lectures on Hoare logic and weakest precondition calculus) are insufficient to learn proof of programs. We discuss the difficulties of the lesson for a student, necessary background, most frequent mistakes, and emphasize some points that often remain misunderstood. This lesson assumes that students have learned the basics of formal specification such as precondition, postcondition, invariant, variant, assertion.

Nikolai Kosmatov, Virgile Prevosto and Julien Signoles
Specification and Proof of Programs with Frama-C [link]
In 28th Symposium on Applied Computing (SAC), 2013