Frama-C/Eva: a concrete application of abstract interpretation
André Maroneze (CEA LIST)
July 16, 2025
The C language is widely used for critical systems, despite its memory unsafety. The Frama-C platform provides static and dynamic code analyses, based on formal verification techniques, to provide guarantees for C code bases. Between testing and full program proof, the Eva analyzer allows automatic identification of several kinds of undefined behaviors. It can be seen as an “abstract debugger”, and help understand what the code does. With some experience, it can scale up to 100k’s lines of code. This presentation will focus on practical examples, some theoretical foundations, and ongoing challenges concerning the application of abstract interpretation to C code analysis.