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


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
Baptiste Pollien, PhD
Software Engineer HMI

I am a Software Engineer HMI at Ampere Software Technology.