TY - GEN
T1 - Frama-C
T2 - 10th International Conference on Software Engineering and Formal Methods, SEFM 2012
AU - Cuoq, Pascal
AU - Kirchner, Florent
AU - Kosmatov, Nikolai
AU - Prevosto, Virgile
AU - Signoles, Julien
AU - Yakobowski, Boris
PY - 2012/11/6
Y1 - 2012/11/6
N2 - 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 analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.
AB - 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 analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.
UR - https://www.scopus.com/pages/publications/84868218937
U2 - 10.1007/978-3-642-33826-7_16
DO - 10.1007/978-3-642-33826-7_16
M3 - Conference contribution
AN - SCOPUS:84868218937
SN - 9783642338250
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 233
EP - 247
BT - Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings
Y2 - 1 October 2012 through 5 October 2012
ER -