Skip to Main content Skip to Navigation
Conference papers

Frama-C, A collaborative framework for C code verification: Tutorial synopsis

Abstract : Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety-and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language, ACSL. This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs.
Document type :
Conference papers
Complete list of metadata
Contributor : Léna Le Roy Connect in order to contact the contributor
Submitted on : Wednesday, July 11, 2018 - 10:02:06 AM
Last modification on : Thursday, February 17, 2022 - 10:08:05 AM



N. Kosmatov, J. Signoles. Frama-C, A collaborative framework for C code verification: Tutorial synopsis. Runtime Verification. RV 2016. Lecture Notes in Computer Science, Sep 2016, madrid, Spain. pp.92-115, ⟨10.1007/978-3-319-46982-9_7⟩. ⟨cea-01834973⟩



Record views