Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs

Résumé

Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.
Fichier non déposé

Dates et versions

hal-01423641 , version 1 (30-12-2016)

Identifiants

Citer

Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue. Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. 2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2016, Raleigh, NC, United States. pp.6, ⟨10.1109/SCAM.2016.18⟩. ⟨hal-01423641⟩
245 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More