Date: Thursday, March 3 2026 – 13h00
Place: C005
Title: Deductive and Collaborative Verification of Implementations with Frama-C
While ensuring the correctness of an implementation based on a formal functional specification provides extremely strong guarantees, it can be very expensive to achieve. In practice, a combination of formal methods is commonly employed to attain an appropriate level of assurance. This includes static analyses to ensure the absence of runtime errors, deductive verification for functional correctness, and dynamic verification. Frama-C is a source code analysis platform designed for the verification of large-scale programs written in ISO C source code. It offers comprehensive support for the integration of formal methods, offering users a set of plug-ins that facilitate static and dynamic analysis of safety-critical and security-critical software. Furthermore, the collaborative verification capabilities are achieved through the integration of these plug-ins on a shared kernel and their adherence to a standardised specification language known as ACSL (ANSI/ISO C Specification Language).
In this talk, I will present specification choices, difficulties and limitations we faced in verification efforts with Frama-C, illustrate them with examples from several case studies and describe solutions that allowed us to verify functional properties, the absence of runtime errors, as well as more high-level properties. While it is often possible to find workarounds when facing Frama-C limitations, this also calls for improvements of the tool. I will discuss some ongoing research in these directions especially in the context of the ANR project CoMeMoV and the ASTRID project VéDySec.
This is joint work with Nikolai Kosmatov, Allan Blanchard, Yani Ziani, Téo Bernier, Daniel Gracia Pérez, Dara Ly, Julien Signoles, Loïc Correnson, Jérémy Damour, Myriam Clouet.