Guide to Software Verification with Frama-C: Core Components, Usages, and Applications (Computer Science Foundations and Applied Logic)

Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications.

Nikolai Kosmatov is a research engineer at Thales Research & Technology since 2019, where he leads the Formal Methods group. His main focus is applying formal methods based techniques and tools (including Frama-C) to industrial projects. Previously, he worked for 13 years at CEA List as an expert researcher in the Frama-C team at Software Safety and Security Lab (LSL). He obtained Ph.D. in Mathematics in 2001 from St.Petersburg State Univ., MS in Computer Science in 2003 from Univ. of Besançon, and Habilitation in Computer Science (HDR) from Univ. Paris-Sud in 2018. His research interests include software testing, formal verification, combinations between static and dynamic analysis techniques, and runtime verification. He co-authored four patents and more than 90 scientific papers in international conferences and journals. He was PC co-chair of several international events related to verification and testing, e.g., TAP 2015, IFIP-ICTSS 2019, ACM SAC-SVT 2020 and 2021. He is co-responsible for the working group on software testing (MTV2) of the French CNRS network on Programming and Software Engineering (GDR GPL) and organizes its annual workshops. Dr. Kosmatov contributed to the design and development of several software verification tools. He is the main author of the PathCrawler-online.com testing web service. 

Virgile Prevosto is a researcher, senior expert in static analysis and formal methods at Université Paris-Saclay, CEA, List, where he works since 2006 in the Software Safety and Security Lab (LSL). After an engineering degree and MS in Computer Science at École Polytechnique (France), he got a Ph.D. in Computer Science from Univ. Paris 6 (now Sorbonne Université) in 2003. He has been one of the main developers of the Frama-C platform nearly since its inception and co-authored more than 25 peer-reviewed papers on Frama-C-related topics. He gave tutorials and training sessions on Frama-C in various academic and industrial venues and teaches static analysis and Frama-C for more than ten years at ENSIIE. He was a co-chair of the program committee of the Formal IDE (F-IDE) workshops in 2018 and 2019 and TAP conference in 2023. He has been CEA List’s principal investigator in many collaborative projects at national and European levels, including the technical coordination of U3CAT (French ANR), Device-Soft (French/German Projet Inter Carnot Fraunhofer), and Decoder (H2020).

Julien Signoles is a research director at Université Paris-Saclay, CEA, List, where he works since 2006 in the Software Safety and Security Lab (LSL). He got a Ph.D. in Computer Science from University Paris-Sud (now University Paris-Saclay, France) in 2006 and an Habilitation (HDR) from the same university in 2018. His research focuses on runtime annotation checking and applications of formal methods to code safety and security. He is one of the main contributors to Frama-C since its conception. In particular, he is the scientific head of E-ACSL, theruntime annotation checker of Frama-C. He published more than 50 peer-reviewed papers on Frama-C-related topics. He teaches formal methods in French universities and engineering schools, and has given plenty of Frama-C tutorials and talks to a broad audience including students, academic researchers, as well as engineers and decision-makers from industry. He has been the CEA List's principal investigator in many French and European projects. He is co-responsible for the working group on Languages and Program Verification (LVP) of the French CNRS network on Programming and Software Engineering (GDR GPL) and scientific advisor of the Department of Software and System Engineering at CEA List.