Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form

Loïc Besnard, Thierry Gautier, Matthieu Moy, Jean-Pierre Talpin, Kenneth Johnson, Florence Maraninchi

Abstract


We present an approach for the translation of imperative code (like
C, C++) into the synchronous formalism Signal, in order to use a
model-checker to verify properties on the source code. The
translation uses SSA as an intermediate formalism, and the GCC
compiler as a front-end. The contributions of this paper with
respect to previous work are a more efficient translation scheme,
and the management of parallel code. It is applied successfully on
simple SystemC examples.

Full Text: PDF