@inproceedings{BGM+09,
title = { {A}utomatic translation of {C}/{C}++ parallel code into synchronous formalism using an {SSA} intermediate form },
author = {Besnard, Lo\"ic and Gautier, Thierry and Moy, Matthieu and Talpin, Jean-Pierre and Johnson, Kenneth and Maraninchi, Florence},
month = {September},
year = {2009},
booktitle = {Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09)},
publisher = {Electronic Communications of the EASST},
team = {SYNC},
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. },
}
