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. },


Contact | Plan du site | Site réalisé avec SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4000879