Conc2seq

Overview

Conc2seq is dedicated to the verification of concurrent C programs. More specifically, it proposes an instrumentation of the original code that simulates all possible interleavings allowed by the C standard. The resulting instrumented code is then a sequential program that can be analyzed as such. Note however that the transformation assumes that the original code is sequentially consistent, which must be verified independently (e.g. by using the Mthread plugin).

Usage

Conc2Seq is available as an external open-source plug-in.

Once installed, it is enabled with the -c2s option, which will generate a sequential version of the concurrent API implementation provided to Frama-C. The generated code and specification is available a new project. To output this simulating program into a file, use the option -c2s-output filename.