@inproceedings(alur2008symbolicanalysisforcoveragesimulinkstateflow,
 author       = {Rajeev Alur and Aditya Kanade and S Ramesh and KC Shashidhar},
 year         = {2008},
 title        = {{Symbolic Analysis for Improving Simulation Coverage of Simulink/Stateflow Models}},
 booktitle    = {{Proceedings of the 8th ACM International Conference on Embedded Software}},
 pages        = {89--98},
 doi          = {10.1145/1450058.1450071},
)
@inproceedings(banphawatthanarak1999symbolic,
 author       = {Chonlawit Banphawatthanarak and Bruce H Krogh and Ken Butts},
 year         = {1999},
 title        = {{Symbolic Verification of Executable Control Specifications}},
 booktitle    = {{Proceedings of the 1999 IEEE International Symposium on Computer Aided Control System Design}},
 organization = {IEEE},
 pages        = {581--586},
 doi          = {10.1109/CACSD.1999.808712},
)
@techreport(barret15smtlib,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2015},
 title        = {{The SMT-LIB Standard: Version 2.5}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 note         = {Available at {\tt www.SMT-LIB.org}},
)
@inbook(barrett18smtbookchapter,
 author       = {Clark Barrett and Cesare Tinelli},
 year         = {2018},
 title        = {Satisfiability Modulo Theories},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-10575-8_11},
)
@article(biere2003boundedmodelchecking,
 author       = {Armin Biere and Alessandro Cimatti and Edmund M Clarke and Ofer Strichman and Yunshan Zhu},
 year         = {2003},
 title        = {{Bounded Model Checking.}},
 journal      = {{Advances in Computers}},
 volume       = {58},
 number       = {11},
 pages        = {117--148},
 doi          = {10.1016/S0065-2458(03)58003-2},
)
@article(bourbouh2017automatedanalysisofstateflowmodels,
 author       = {Hamza Bourbouh and Pierre-Loic Garoche and Christophe Garion and Arie Gurfinkel and Kahsai Temesghen and Xavier Thirioux},
 year         = {2017},
 title        = {{Automated Analysis of Stateflow Models}},
 doi          = {10.29007/b8gq},
)
@inproceedings(bourbouh2020cocosim,
 author       = {Hamza Bourbouh and Pierre-Lo{\"\i}c Garoche and Thomas Loquen and {\'E}ric Noulard and Claire Pagetti},
 year         = {2020},
 title        = {{CoCoSim, a Code Generation Framework for Control/Command Applications: An Overview of CoCoSim for Multi-periodic Discrete Simulink Models}},
 booktitle    = {10th European Congress on Embedded Real Time Software and Systems (ERTS 2020)},
)
@inproceedings(champion16kind2,
 author       = {Adrien Champion and Alain Mebsout and Christoph Sticksel and Cesare Tinelli},
 year         = {2016},
 title        = {{The Kind~2 Model Checker}},
 booktitle    = {International Conference on Computer Aided Verification},
 organization = {Springer},
 pages        = {510--517},
 doi          = {10.1007/978-3-319-41540-6_29},
)
@inproceedings(chen10formalanalysisofstateflowdiagrams,
 author       = {C. {Chen}},
 year         = {2010},
 title        = {{Formal Analysis for Stateflow Diagrams}},
 booktitle    = {2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion},
 pages        = {102--109},
 doi          = {10.1109/SSIRI-C.2010.29},
)
@inproceedings(demoura08z3,
 author       = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3: An Efficient SMT Solver}},
 booktitle    = {Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {TACAS'08/ETAPS'08},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
 url          = {http://dl.acm.org/citation.cfm?id=1792734.1792766},
)
@inproceedings(demoura03BMCrefutationtoverification,
 author       = {De Moura, Leonardo and Rue{\ss}, Harald and Maria Sorea},
 year         = {2003},
 title        = {{Bounded Model Checking and Induction: From Refutation to Verification}},
 booktitle    = {International Conference on Computer Aided Verification},
 organization = {Springer},
 pages        = {14--26},
 doi          = {10.1007/978-3-540-45069-6_2},
)
@inproceedings(duggirala15c2e2,
 author       = {Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan and Matthew Potok},
 year         = {2015},
 title        = {{C2E2: A Verification Tool for Stateflow Models}},
 booktitle    = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {68--82},
 doi          = {10.1007/978-3-662-46681-0_5},
)
@incollection(etienne10usingsldv,
 author       = {J-F Etienne and S Fechter and E Juppeaux},
 year         = {2010},
 title        = {Using simulink design verifier for proving behavioral properties on a complex safety critical system in the ground transportation domain},
 booktitle    = {Complex Systems Design \& Management},
 publisher    = {Springer},
 pages        = {61--72},
 doi          = {10.1007/978-3-642-15654-0_4},
)
@misc(sesfGitLink,
 author       = {Predrag Filipovikj},
 year         = {2021},
 title        = {{SESf tool}},
 howpublished = {\url{https://github.com/predragf/sesf}},
 note         = {[Online; accessed: September 21, 2022]},
)
@article(filipovikj21bicforstateflowprogramsarxiv,
 author       = {Predrag Filipovikj and Dilian Gurov and Mattias Nyberg},
 year         = {2021},
 title        = {{Bounded Invariant Checking for Stateflow Programs}},
 journal      = {CoRR},
 volume       = {abs/2103.06248},
 eprint       = {2103.06248},
)
@article(godefroid05dartconcolictesting,
 author       = {Patrice Godefroid and Nils Klarlund and Koushik Sen},
 year         = {2005},
 title        = {DART: Directed Automated Random Testing},
 journal      = {SIGPLAN Not.},
 volume       = {40},
 number       = {6},
 pages        = {213–223},
 doi          = {10.1145/1064978.1065036},
)
@inproceedings(hamon2005denotational,
 author       = {Gr{\'e}goire Hamon},
 year         = {2005},
 title        = {{A Denotational Semantics for Stateflow}},
 booktitle    = {{Proceedings of the 5th ACM international conference on Embedded software}},
 pages        = {164--172},
 doi          = {10.1145/1086228.1086260},
)
@inproceedings(hamon2008simulink,
 author       = {Gr{\'e}goire Hamon},
 year         = {2008},
 title        = {{Simulink Design Verifier - Applying Automated Formal Methods to Simulink and Stateflow}},
 booktitle    = {Third Workshop on Automated Formal Methods},
 note         = {Invited paper.},
)
@inproceedings(hamon2004operationalsemanticsstateflow,
 author       = {Gr{\'e}goire Hamon and John Rushby},
 year         = {2004},
 title        = {{An Operational Semantics for Stateflow}},
 booktitle    = {{International Conference on Fundamental Approaches to Software Engineering}},
 organization = {Springer},
 pages        = {229--243},
 doi          = {10.1007/978-3-540-24721-0_17},
)
@article(hamon2007operationalsemanticsstateflow,
 author       = {Gr{\'e}goire Hamon and John Rushby},
 year         = {2007},
 title        = {{An Operational Semantics for Stateflow}},
 journal      = {{International Journal on Software Tools for Technology Transfer}},
 volume       = {9},
 number       = {5-6},
 pages        = {447--456},
 doi          = {10.1007/s10009-007-0049-7},
)
@article(harel1987statecharts,
 author       = {David Harel},
 year         = {1987},
 title        = {{Statecharts: A Visual Formalism for Complex Systems}},
 journal      = {{Science of Computer Programming}},
 volume       = {8},
 number       = {3},
 pages        = {231--274},
 doi          = {10.1016/0167-6423(87)90035-9},
)
@misc(iso26262,
 author       = {ISO},
 year         = {{2011}},
 title        = {{Road vehicles -- Functional safety}},
)
@article(jiang2019dependablecpsstateflow,
 author       = {Yu Jiang and Houbing Song and Yixiao Yang and Han Liu and Ming Gu and Yong Guan and Jiaguang Sun and Lui Sha},
 year         = {2019},
 title        = {{Dependable Model-driven Development of CPS: From Stateflow Simulation to Verified Implementation}},
 journal      = {{ACM Transactions on Cyber-Physical Systems}},
 volume       = {3},
 number       = {1},
 pages        = {12},
 doi          = {10.1145/3078623},
)
@inproceedings(kaalen22stateflowstochastic,
 author       = {Stefan Kaalen and Anton Hampus and Mattias Nyberg and Olle Mattsson},
 year         = {2022},
 title        = {A Stochastic Extension of Stateflow},
 booktitle    = {Proceedings of the 2022 ACM/SPEC on International Conference on Performance Engineering},
 series       = {ICPE '22},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {211–222},
 doi          = {10.1145/3489525.3511679},
)
@article(king1976symbolicexecutionandtesting,
 author       = {James C King},
 year         = {1976},
 title        = {{Symbolic Execution and Program Testing}},
 journal      = {{Communications of the ACM}},
 volume       = {19},
 number       = {7},
 pages        = {385--394},
 doi          = {10.1145/360248.360252},
)
@inproceedings(meenakshi2006toolfortranslatingsimulink,
 author       = {B Meenakshi and Abhishek Bhatnagar and Sudeepa Roy},
 year         = {2006},
 title        = {{Tool for Translating Simulink Models into Input Language of a Model Checker}},
 booktitle    = {{International Conference on Formal Engineering Methods}},
 organization = {Springer},
 pages        = {606--620},
 doi          = {10.1007/11901433_33},
)
@article(miyazawa12refinementorientedmodelsofstateflow,
 author       = {Alvaro Miyazawa and Ana Cavalcanti},
 year         = {2012},
 title        = {{Refinement-oriented Models of Stateflow Charts}},
 journal      = {Science of Computer Programming},
 volume       = {77},
 number       = {10-11},
 pages        = {1151--1177},
 doi          = {10.1016/j.scico.2011.07.007},
)
@inproceedings(pilaud1987lustre,
 author       = {Daniel Pilaud and N Halbwachs and JA Plaice},
 year         = {1987},
 title        = {{LUSTRE: A Declarative Language for Programming Synchronous Systems}},
 booktitle    = {Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages (14th POPL 1987). ACM, New York, NY},
 volume       = {178},
 pages        = {188},
 doi          = {10.1145/41625.41641},
)
@misc(simulinkug,
 author       = {The MathWorks, Inc.},
 year         = {2020},
 title        = {{Matlab\&Simulink - Simulink User's Guide}},
 howpublished = {\url{https://www.mathworks.com/help/pdf_doc/simulink/simulink_ug.pdf}},
 note         = {[Online; accessed: September 21, 2022]},
)
@misc(stateflowug,
 author       = {The MathWorks, Inc.},
 year         = {2020},
 title        = {{Matlab\&Simulink - Stateflow User's Guide}},
 howpublished = {\url{https://www.mathworks.com/help/pdf_doc/stateflow/stateflow_ug.pdf}},
 note         = {[Online; accessed: September 21, 2022]},
)
@inproceedings(yang16stateflowtransformationase,
 author       = {Yixiao Yang and Yu Jiang and Ming Gu and Jiaguang Sun},
 year         = {2016},
 title        = {{Verifying Simulink Stateflow Model: Timed Automata Approach}},
 booktitle    = {{Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering}},
 series       = {ASE 2016},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {852--857},
 doi          = {10.1145/2970276.2970293},
)
@inproceedings(zuliani10bayesiansimulinkstateflow,
 author       = {Paolo Zuliani and Andr{\'e} Platzer and Edmund M Clarke},
 year         = {2010},
 title        = {{Bayesian Statistical Model Checking with Application to Simulink/Stateflow Verification}},
 booktitle    = {Proceedings of the 13th ACM international conference on Hybrid systems: computation and control},
 pages        = {243--252},
 doi          = {10.1145/1755952.1755987},
)