A Lesson on Verification of IoT Software with Frama-C

Abstract

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.

Publication
International Conference on High Performance Computing and Simulation (HPCS)
Date
Links
DOI