@inproceedings{eef26c9a50b94ec5afad0f7f910354bb,
title = "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.",
keywords = "ACSL, Abstract interpretation, Combinations of analyses, Deductive verification, Frama-C, Runtime verification, Test generation",
author = "Nikolai Kosmatov and Julien Signoles",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 16th International Conference on Runtime Verification, RV 2016 ; Conference date: 23-09-2016 Through 30-09-2016",
year = "2016",
month = jan,
day = "1",
doi = "10.1007/978-3-319-46982-9\_7",
language = "English",
isbn = "9783319469812",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "92--115",
editor = "Yli{\`e}s Falcone and C{\'e}sar S{\'a}nchez",
booktitle = "Runtime Verification - 16th International Conference, RV 2016, Proceedings",
}