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 metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834973
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:06 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

44