M. Mark, P. B. Adams, and . Clayton, ClawZ: Cost-Effective Formal Verification for Control Systems, 7th Int. Conf. on Formal Methods and Software Engineering (ICFEM 2005) (LNCS), vol.3785, pp.465-479, 2005.

R. Alur, A. Kanade, S. Ramesh, and K. C. Shashidhar, Symbolic Analysis for Improving Simulation Coverage of Simulink/Stateflow Models, Proc. 8th ACM Int. Conf. on Embedded Software, pp.89-98, 2008.

R. D. Arthan, P. Caseley, C. O'halloran, and A. Smith, ClawZ: control laws in Z, 2nd Int. Conf. on Formal Methods and Software Engineering, pp.169-176, 2000.

C. Auger, Compilation certifiée de SCADE/LUSTRE, Ph.D. Dissertation. Univ. Paris Sud, vol.11, 2013.

C. Auger, J. Colaço, G. Hamon, and M. Pouzet, A Formalization and Proof of a Modular Lustre Code Generator, 2014.

G. Berry, Real Time Programming: Special Purpose or General Purpose Languages, Proc. 11th Int. Federation for Information Processing, pp.11-17, 1989.
URL : https://hal.archives-ouvertes.fr/inria-00075494

G. Berry, Preemption in Concurrent Systems, Foundations of Software Technology and Theoretical Computer Science (LNCS), vol.761, pp.72-93, 1993.

G. Berry, The Esterel v5 Language Primer (5.91 ed.). Ecole des Mines and INRIA, 2000.

G. Berry, The Constructive Semantics of Pure Esterel (draft version 3 ed.), 2002.

D. Biernacki, J. Colaço, G. Hamon, and M. Pouzet, Clock-directed modular code generation for synchronous data-flow languages, Proc. 9th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2008), pp.121-130, 2008.

S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, J. Automated Reasoning, vol.43, pp.263-288, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00352524

O. Bouissou and A. Chapoutot, An operational semantics for Simulink's simulation engine, Proc. 13th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2012, pp.129-138, 2012.

T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet et al., A Formally Verified Compiler for Lustre, Proc. 2017 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), 2017.
URL : https://hal.archives-ouvertes.fr/hal-01512286

, , pp.586-601

T. Bourke, L. Brun, and M. Pouzet, Towards a verified Lustre compiler with modular reset, Proc. 21st Int. Workshop on Software and Compilers for Embedded Systems (SCOPES'18), pp.14-17, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01817949

T. Bourke and M. Pouzet, Arguments cadencés dans un compilateur Lustre vérifié, 30 ièmes Journées Francophones des Langages Applicatifs, pp.109-124, 2019.

P. Caspi, Clocks in dataflow languages, Theoretical Computer Science, vol.94, issue.1, pp.125-140, 1992.

P. Caspi, Towards recursive block diagrams, Annual Review in Automatic Programming, vol.18, pp.90015-90024, 1994.

P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice, LUSTRE: A declarative language for programming synchronous systems, Proc. 14th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.178-188, 1987.

P. Caspi and M. Pouzet, A Co-iterative Characterization of Synchronous Stream Functions, 1997.
URL : https://hal.archives-ouvertes.fr/hal-01622305

P. Caspi and M. Pouzet, A Co-iterative Characterization of Synchronous Stream Functions, First Workshop on Coalgebraic Methods in Computer Science (CMCS'98) (ENTCS), vol.11, pp.50-57, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01622305

A. Cavalcanti, P. Clayton, and C. Halloran, From control law diagrams to Ada via Circus, Formal Aspects of Computing, vol.23, pp.465-512, 2011.

A. Chapoutot and M. Martel, Abstract Simulation: A Static Analysis of Simulink Models, Proc. Int. Conf. on Embedded Software and Systems, pp.83-92, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00332447

C. Chen, J. S. Dong, and J. Sun, A formal framework for modeling and validating Simulink diagrams, Formal Aspects of Computing, vol.21, pp.451-483, 2009.

M. Chen, X. Han, T. Tang, S. Wang, M. Yang et al., MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems, Provably Correct Systems (NASA Monographs in Systems and Software Engineering, pp.39-58, 2017.

A. Cohen, L. Gérard, and M. Pouzet, Programming Parallelism with Futures in Lustre, Proc. 12th ACM Int. Conf. on Embedded Software (EMSOFT 2012, pp.197-206, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00786682

J. Colaço, B. Pagano, and M. Pouzet, A Conservative Extension of Synchronous Data-flow with State Machines, Proc. 5th ACM Int. Conf. on Embedded Software (EMSOFT 2005), pp.173-182, 2005.

J. Colaço, B. Pagano, and M. Pouzet, Scade 6: A Formal Language for Embedded Critical Software Development, Proc. 11th Int. Symp. Theoretical Aspects of Software Engineering, pp.4-15, 2017.

J. Colaço and M. Pouzet, Clocks as First Class Abstract Types, Proc. 3rd Int. Conf. on Embedded Software (EMSOFT 2003) (LNCS), vol.2855, pp.134-155, 2003.

J. Colaço and M. Pouzet, Type-based initialization analysis of a synchronous dataflow language, Int. J. Software Tools for Technology Transfer, vol.6, pp.245-255, 2004.

, The Coq proof assistant reference manual, 2019.

L. Gérard, A. Guatto, C. Pasteur, and M. Pouzet, A modular memory optimization for synchronous data-flow languages: application to arrays in a Lustre compiler, Proc. 13th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2012, pp.51-60, 2012.

G. Hamon, A Denotational Semantics for Stateflow, Proc. 5th ACM Int. Conf. on Embedded Software (EMSOFT 2005), pp.164-172, 2005.

G. Hamon and M. Pouzet, Modular Resetting of Synchronous Data-Flow Programs, Proc. 2nd ACM SIGPLAN Int. Conf. on Principles and Practice of Declarative Programming, pp.289-300, 2000.
URL : https://hal.archives-ouvertes.fr/hal-01573195

G. Hamon and J. Rushby, An Operational Semantics for Stateflow, Proc. 7th Int. Conf. on Fundamental Approaches to Software Engineering (FASE'04), vol.2984, pp.229-243, 2004.

D. Harel, Statecharts: A Visual Formalism for Complex Systems, Science of Computer Programming, vol.8, issue.3, pp.90035-90044, 1987.

D. Harel and A. Naamad, The STATEMATE Semantics of Statecharts. ACM Trans. Software Engineering and Methodology (TOSEM), vol.5, pp.293-333, 1996.

E. Jahier, P. Raymond, and N. Halbwachs, The Lustre V6 Reference Manual, 2019.

J. Jourdan, F. Pottier, and X. Leroy, Validating LR(1) parsers, 21st European Symposium on Programming (ESOP 2012), held as part of European Joint Conferences on Theory and Practice of Software (ETAPS 2012) (LNCS), Helmut Seidl, vol.7211, pp.397-416, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01077321

G. Kahn, The Semantics of a Simple Language for Parallel Programming, Proc. Int. Federation for Information Processing, pp.471-475, 1974.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: A Verified Implementation of ML, Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.179-191, 2014.

X. Leroy, Formal verification of a realistic compiler, Comms. ACM, vol.52, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

F. Maraninchi and N. Halbwachs, Compiling Argos into Boolean equations, Proc. 4th Int. Symp. Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT '96) (LNCS), vol.1135, pp.72-89, 1996.

F. Maraninchi and Y. Rémond, Argos: an automaton-based synchronous language, Computer Languages, vol.27, pp.61-92, 2001.
URL : https://hal.archives-ouvertes.fr/hal-00273055

F. Maraninchi, Y. Rémond, ;. Van-chan, J. Ngo, T. Talpin et al., Mode-Automata: a new Domain-Specific Construct for the Development of Safe Critical Systems, Proc. 35th IFIP WG 6.1 Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015) (LNCS), vol.46, pp.66-80, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01876521

C. Paulin-mohring, A constructive denotational semantics for Kahn networks in Coq, From Semantics to Computer Science: Essays in Honour of Gilles Kahn, pp.383-413, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00431806

, Haskell 98 Language and Libraries: The Revised Report, CUP, 2003.

D. Potop, -. Butucaru, S. A. Edwards, and G. Berry, Compiling Esterel, 2007.

M. Pouzet, Lucid Synchrone, v. 3. Tutorial and reference manual, 2006.

M. Ryabtsev and O. Strichman, Translation Validation: From Simulink to C, Proc. 21st Int. Conf. on Computer Aided Verification (CAV 2009) (LNCS), vol.5643, pp.696-701, 2009.

G. Shi, Y. Gan, S. Shang, S. Wang, Y. Dong et al., A Formally Verified Sequentializer for Lustre-Like Concurrent Synchronous Data-Flow Programs, Proc. 39th Int. Conf. on Software Engineering Companion (ICSE-C'17), pp.109-111, 2017.

G. Shi, Y. Zhang, S. Shang, S. Wang, Y. Dong et al., A formally verified transformation to unify multiple nested clocks for a Lustre-like language, Science China Information Sciences, vol.62, issue.1, p.12801, 2019.

Y. Tan, M. O. Myreen, R. Kumar, A. Fox, S. Owens et al., A New Verified Compiler Backend for CakeML, Proc. 21st ACM SIGPLAN Int. Conf. on Functional Programming, pp.60-73, 2016.

S. Tripakis, C. Sofronis, P. Caspi, and A. Curic, Translating Discrete-Time Simulink to Lustre, ACM Trans. Embedded Computing Systems, vol.4, pp.779-818, 2005.

C. Zhou and R. Kumar, Semantic Translation of Simulink Diagrams to Input/Output Extended Finite Automata, Discrete Event Dynamic Systems, vol.22, pp.223-247, 2012.

L. Zou, N. Zhan, S. Wang, and M. Fränzle, Formal Verification of Simulink/Stateflow Diagrams, Proc. 13th Int. Symp. Automated Technology for Verification and Analysis (ATVA 2015) (LNCS), Bernd Finkbeiner, vol.9364, pp.464-481, 2015.

L. Zou, N. Zhan, S. Wang, M. Fränzle, and S. Qin, Verifying Simulink Diagrams via a Hybrid Hoare Logic Prover, Proc. 13th ACM Int. Conf. on Embedded Software (EMSOFT 2013, vol.9, pp.1-9, 2013.