A Lesson on Verification of IoT Software with Frama-C
[ 2018 ] Tutorial

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue


This paper is a tutorial introduction to Frama-C, a framework for analysis and verification of C programs. We present value analysis, deductive verification and runtime verification of software using Frama-C and in particular its EVA, WP, and E-ACSL plugins. These techniques are illustrated on examples coming from real-life verification case studies for different modules of Contiki, a lightweight operating system for the Internet of Things.


Proc. of the 12th International Conference on High Performance Computing & Simulation (HPCS 2018)

Orléans, France, July 2018, pages 21-30. IEEE. ISBN 978-1-5386-7878-7.

Final publication available at http://ieeexplore.ieee.org/. DOI: 10.1109/HPCS.2018.00018.

Paper (Available PDF is the author's final version of the work)