A. Agrawal, G. Simon, and G. Karsai, Semantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations, Electronic Notes in Theoretical Computer Science, vol.109, pp.43-56, 2004.
DOI : 10.1016/j.entcs.2004.02.055

C. Chen, J. S. Dong, and J. Sun, A formal framework for modeling and validating Simulink diagrams, Formal Aspects of Computing, vol.40, issue.5, pp.451-483, 2009.
DOI : 10.1007/s00165-009-0108-9

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

D. Moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

E. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.
DOI : 10.1145/360933.360975

I. Dragomir, V. Preoteasa, and S. Tripakis, Compositional Semantics and Analysis of Hierarchical Block Diagrams, SPIN, pp.38-56, 2016.
DOI : 10.1007/978-3-319-32582-8_3

B. Dutertre and L. De-moura, The Yices SMT solver, 2006.

F. Haftmann and M. Wenzel, Constructive Type Classes in Isabelle, TYPES, pp.160-174, 2007.
DOI : 10.1007/978-3-540-74464-1_11

X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. Butts, Powertrain control verification benchmark, Proceedings of the 17th international conference on Hybrid systems: computation and control, HSCC '14, pp.253-262, 2014.
DOI : 10.1145/2562059.2562140

B. Meenakshi, A. Bhatnagar, and S. Roy, Tool for Translating Simulink Models into Input Language of a Model Checker, ICFEM, 2006.
DOI : 10.1007/11901433_33

S. Minopoli and G. Frehse, SL2SX Translator, Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC '16, pp.93-98, 2016.
DOI : 10.1109/EMSOFT.2013.6658587

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic, 2002.
DOI : 10.1007/3-540-45949-9

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, CADE, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

V. Preoteasa, I. Dragomir, and S. Tripakis, Type Inference of Simulink Hierarchical Block Diagrams in Isabelle, 1612.
DOI : 10.1109/EMSOFT.2013.6658587

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

V. Preoteasa and S. Tripakis, Refinement calculus of reactive systems, Proceedings of the 14th International Conference on Embedded Software, EMSOFT '14, pp.1-2, 2014.
DOI : 10.1145/2656045.2656068

V. Preoteasa and S. Tripakis, Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, 2016.
DOI : 10.1145/292540.292560

R. Reicherdt and S. Glesner, Formal Verification of Discrete-Time MAT- LAB/Simulink Models Using Boogie, In SEFM, pp.190-204, 2014.

P. Roy and N. Shankar, SimCheck: a contract type system for Simulink, Innovations in Systems and Software Engineering, pp.73-83, 2011.
DOI : 10.1145/1113830.1113834

V. Sfyrla, G. Tsiligiannis, I. Safaka, M. Bozga, and J. Sifakis, Compositional translation of simulink models into synchronous BIP, International Symposium on Industrial Embedded System (SIES), pp.217-220, 2010.
DOI : 10.1109/SIES.2010.5551374

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

S. Tripakis, B. Lickly, T. A. Henzinger, and E. A. Lee, A Theory of Synchronous Relational Interfaces, ACM Trans. Program. Lang. Syst, vol.3314, issue.4, pp.1-1441, 2011.

S. Tripakis, C. Pinello, A. Benveniste, A. Sangiovanni-vincentelli, P. Caspi et al., Implementing Synchronous Models on Loosely Time Triggered Architectures, IEEE Transactions on Computers, vol.57, issue.10, pp.1300-1314, 2008.
DOI : 10.1109/TC.2008.81

S. Tripakis, C. Sofronis, P. Caspi, and A. Curic, Translating discrete-time simulink to lustre, ACM Transactions on Embedded Computing Systems, vol.4, issue.4, pp.779-818, 2005.
DOI : 10.1145/1113830.1113834

URL : http://www-verimag.imag.fr/~curic/translatingDTsimulink.pdf

C. Yang and V. Vyatkin, Transformation of Simulink models to IEC 61499 Function Blocks for verification of distributed control systems, Control Engineering Practice, vol.20, issue.12, pp.1259-1269, 2012.
DOI : 10.1016/j.conengprac.2012.06.008

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

L. Zou, N. Zhany, S. Wang, M. Franzle, and S. Qin, Verifying Simulink diagrams via a Hybrid Hoare Logic Prover, 2013 Proceedings of the International Conference on Embedded Software (EMSOFT), pp.1-910, 2013.
DOI : 10.1109/EMSOFT.2013.6658587