Frama-C: A software analysis perspective - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Article Dans Une Revue Formal Aspects of Computing Année : 2015

Frama-C: A software analysis perspective

Florent Kirchner
  • Fonction : Auteur
  • PersonId : 975105
Nikolai Kosmatov
  • Fonction : Auteur
  • PersonId : 940734
Virgile Prévosto
Julien Signoles
Boris Yakobowski

Résumé

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
Fichier principal
Vignette du fichier
FRAMA.pdf (1.07 Mo) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

cea-01808981 , version 1 (21-02-2024)

Identifiants

Citer

Florent Kirchner, Nikolai Kosmatov, Virgile Prévosto, Julien Signoles, Boris Yakobowski. Frama-C: A software analysis perspective. Formal Aspects of Computing, 2015, 27 (3), pp.573 - 609. ⟨10.1007/s00165-014-0326-7⟩. ⟨cea-01808981⟩
181 Consultations
8 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More