Frama-C: A software analysis perspective

Florent Kirchner; Nikolai Kosmatov; Virgile Prevosto; Julien Signoles; Boris Yakobowski

doi:10.1007/s00165-014-0326-7

Frama-C: A software analysis perspective

Florent Kirchner
, Nikolai Kosmatov
, Virgile Prevosto
, Julien Signoles
, Boris Yakobowski

CEA/UVSQ/CNRS

Research output: Contribution to journal › Article › peer-review

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

Original language	English
Pages (from-to)	573-609
Number of pages	37
Journal	Formal Aspects of Computing
Volume	27
Issue number	3
DOIs	https://doi.org/10.1007/s00165-014-0326-7
Publication status	Published - 1 May 2015
Externally published	Yes

Keywords

C
Dynamic analysis
Formal verification
Static analysis

Access to Document

10.1007/s00165-014-0326-7

Cite this

@article{40c7f580adeb4bf88841d0958a4a21a2,

title = "Frama-C: A software analysis perspective",

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 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.",

keywords = "C, Dynamic analysis, Formal verification, Static analysis",

author = "Florent Kirchner and Nikolai Kosmatov and Virgile Prevosto and Julien Signoles and Boris Yakobowski",

note = "Publisher Copyright: {\textcopyright} 2015, British Computer Society.",

year = "2015",

month = may,

day = "1",

doi = "10.1007/s00165-014-0326-7",

language = "English",

volume = "27",

pages = "573--609",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

number = "3",

}

TY - JOUR

T1 - Frama-C

T2 - A software analysis perspective

AU - Kirchner, Florent

AU - Kosmatov, Nikolai

AU - Prevosto, Virgile

AU - Signoles, Julien

AU - Yakobowski, Boris

PY - 2015/5/1

Y1 - 2015/5/1

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.

KW - C

KW - Dynamic analysis

KW - Formal verification

KW - Static analysis

U2 - 10.1007/s00165-014-0326-7

DO - 10.1007/s00165-014-0326-7

M3 - Article

AN - SCOPUS:84939953549

SN - 0934-5043

VL - 27

SP - 573

EP - 609

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 3

ER -

Frama-C: A software analysis perspective

Abstract

Keywords

Access to Document

Fingerprint

Cite this