Tutorials
Frama-C Framework
Allan Blanchard, Nikolai Kosmatov, 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, 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