R. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.35677-691, 1986.
DOI : 10.1109/TC.1986.1676819

M. and L. Borgne, Systèmes dynamiques sur des corps finis, Thèse, 1993.

M. L. Borgne, A. Benveniste, and P. L. Guernic, Dynamical systems over Galois fields and DEDS control problems, [1991] Proceedings of the 30th IEEE Conference on Decision and Control, pp.1505-1509, 1991.
DOI : 10.1109/CDC.1991.261653

L. Besnard, T. Gautier, P. L. Guernic, and J. Talpin, Compilation of Polychronous Data Flow Equations, Synthesis of Embedded Software, 2010.
DOI : 10.1007/978-1-4419-6400-7_1

URL : https://hal.archives-ouvertes.fr/inria-00540493

L. Besnard, T. Gautier, M. Moy, J. Talpin, K. Johnson et al., Automatic translation of C/C ++ parallel code into synchronous formalism using an SSA intermediate form, Proceedings of the 9th Workshop on Automated Verification of Critical Systems AVOCS, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00400272

B. Dutertre, M. L. Borgne, and H. Marchand, SIGALI: un système de calcul formel pour la vérification de programmes SIGNAL, Manuel d'utilisation. Note technique, non publiée, 1998.

A. Gamatié, Designing embedded systems with the SIGNAL programming: Synchronous, Reactive Specification, 2009.

P. , L. Guernic, J. Talpin, and J. Lann, Polychrony for system design, Journal for Circuits Systems and Computers, vol.12, issue.3, pp.261-304, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00730480

N. Halbwachs, A Synchronous Language at Work: The Story of Lustre, 3th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05), 2005.
DOI : 10.1002/9781118459898.ch2

URL : https://hal.archives-ouvertes.fr/hal-00190883

H. Kalla, J. Talpin, D. Berner, and L. Besnard, Automated translation of C/C++ models into a synchronous formalism, 13th Annual IEEE International Symposium and Workshop on Engineering of Computer-Based Systems (ECBS'06), p.6, 2006.
DOI : 10.1109/ECBS.2006.27

URL : https://hal.archives-ouvertes.fr/hal-00546021

O. Kouchnarenko, S. Pinchinat, H. Marchand, H. Rutten, E. L. Borgne et al., Intensional approaches for symbolic methods Formal verification of SIGNAL programs: Application to a power transformer station controller, In Electronic Notes in Theoretical Computer Science In Science of Computer Programming, vol.41, issue.1, pp.85-104, 1998.

V. C. Ngo, J. Talpin, T. Gautier, P. L. Guernic, and L. Besnard, Formal Verification of Compiler Transformations on Polychronous Equations, Processdings of IFM'12, 2012.
DOI : 10.1007/978-3-642-30729-4_9

URL : https://hal.archives-ouvertes.fr/hal-00730393

D. Novillo, Tree ssa -a new high-level optimization framework for the gnu compiler collection, Proceedings of the Nord/USENIX Users Conference, 2003.

D. Novillo, Design and implementation of tree-ssa, GCC Summit Proceedings, 2004.

D. Park, Concurrency and automata on infinite sequences, Proceedings of 5th GI Conf. on Th Comp. Sci, pp.167-183, 1981.
DOI : 10.1007/BFb0017309

J. C. Peralta, T. Gautier, L. Besnard, and P. L. Guernic, LTSs for translation validation of (multi-clocked) SIGNAL specifications, Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010.
DOI : 10.1109/MEMCOD.2010.5558632

URL : https://hal.archives-ouvertes.fr/hal-00555169

S. Pinchinat, H. Marchand, and M. L. Borgne, Symbolic abstractions of automata and their application to the supervisory control problem, In INRIA Technical Reports No 1279, pp.1-29, 1999.

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, 4th Intl. Conf. TACAS'98. LNCS 1384, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

A. Pnueli, O. Shtrichman, and M. Siegel, Translation Validation: From SIGNAL to C, Correct Sytem Design Recent Insights and Advances. LNCS 1710, pp.231-255, 2000.
DOI : 10.1007/3-540-48092-7_11

R. Milner, Operational and Algebraic Semantics of Concurrent Processes, Lab. for Foundations of Computer Science, 1988.
DOI : 10.1016/B978-0-444-88074-1.50024-X

R. Milner, A complete axiomatisation for observational congruence of finite-state behaviors, In SIAM J. Comput, vol.81, issue.2, pp.227-247, 1989.

R. Simone and A. Ressouche, Compositional semantics of Esterel and verification by compositional reductions, Proceedings of CAV'94, 1994.
DOI : 10.1007/3-540-58179-0_74

R. J. Van-glabbeek, The linear time ??? Branching time spectrum II, CONCUR '93: 4th International Conference on Concurrent, pp.66-81, 1993.
DOI : 10.1007/3-540-57208-2_6