Frama-C, A collaborative framework for C code verification: Tutorial synopsis - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Access content directly
Conference Papers Year : 2016

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.
Not file

Dates and versions

cea-01834973 , version 1 (11-07-2018)

Identifiers

Cite

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⟩
86 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More