A gentle introduction to C code verification using the Frama-C platform

Abstract

This document presents a process to verify C programs or librairies using the Frama-C verification tool. Frama-C allows to verify different types of properties on C code, such as the absence of runtime errors or more complex functional properties. The present document is the result of our work on the verification of a mathematical library of the Paparazzi autopilot and is intented to be used as a first guide to formal verification of C programs for Concorde users. In addition to provide a verification process, we also give Frama-C tips and tricks to help users and clarify some points that might not be clear in the official documentation of the tool.

Baptiste Pollien, PhD

Software Engineer HMI

I am a Software Engineer HMI at Ampere Software Technology.