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

Abstract : 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.
Type de document :
Communication dans un congrès
2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2016, Raleigh, NC, United States. IEEE, pp.6, 2016, 〈10.1109/SCAM.2016.18〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01423641
Contributeur : Frédéric Loulergue <>
Soumis le : vendredi 30 décembre 2016 - 18:00:36
Dernière modification le : mercredi 16 mai 2018 - 12:14:01

Identifiants

Citation

Blanchard Allan, 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. IEEE, pp.6, 2016, 〈10.1109/SCAM.2016.18〉. 〈hal-01423641〉

Partager

Métriques

Consultations de la notice

251