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.

In

Proc. of the 16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016)

Raleigh, NC, USA, October 2016, pages 67-72. IEEE. ISBN 978-1-5090-3848-0.

Final publication available at http://link.springer.com. DOI: 10.1007/978-3-319-47166-2_32.

Paper (Available PDF is the author's final version of the work)

Slides