{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:16Z","timestamp":1781193736425,"version":"3.54.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_21","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:31:58Z","timestamp":1781191918000},"page":"456-476","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Formal Verification of\u00a0Hybrid Synchronous Programs with\u00a0Refinement Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9028-6597","authenticated-orcid":false,"given":"Serra Z.","family":"Dane","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5461-6711","authenticated-orcid":false,"given":"Jiawei","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2651-7708","authenticated-orcid":false,"given":"Marc","family":"Pouzet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6378-1447","authenticated-orcid":false,"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol.\u00a0736, pp. 209\u2013229. Springer, Berlin, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30","DOI":"10.1007\/3-540-57318-6_30"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Lectures on Runtime Verification: Introductory and Advanced Topics, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5","DOI":"10.1007\/978-3-319-75632-5_5"},{"issue":"3","key":"21_CR3","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1016\/j.jcss.2011.08.009","volume":"78","author":"A Benveniste","year":"2012","unstructured":"Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci. 78(3), 877\u2013910 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.08.009","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code. In: Proceedings of the Ninth ACM International Conference on Embedded Software - EMSOFT \u201911, p.\u00a0137. ACM Press, Taipei, Taiwan (2011). https:\/\/doi.org\/10.1145\/2038642.2038664","DOI":"10.1145\/2038642.2038664"},{"issue":"1","key":"21_CR5","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., De Simone, R.: The synchronous languages twelve years later. Proc. IEEE 91(1), 64\u201383 (2003). https:\/\/doi.org\/10.1109\/JPROC.2002.805826","journal-title":"Proc. IEEE"},{"key":"21_CR6","unstructured":"Berry, G.: Real time programming: special purpose or general purpose languages. In: Ritter, G. (ed.) Information Processing \u201989: Proceedings of the IFIP 11th World Computer Congress, pp. 11\u201317. Elsevier Science Publishers B.V. (North-Holland) (1989)"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992). https:\/\/doi.org\/10.1016\/0167-6423(92)90005-V","journal-title":"Sci. Comput. Program."},{"key":"21_CR8","doi-asserted-by":"publisher","unstructured":"Bourke, T., Pouzet, M.: Z\u00e9lus: a synchronous language with ODEs. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 113\u2013118 (2013). https:\/\/doi.org\/10.1145\/2461328.2461348","DOI":"10.1145\/2461328.2461348"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 178\u2013188 (1987). https:\/\/doi.org\/10.1145\/41625.41641","DOI":"10.1145\/41625.41641"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Cellier, F.E.: Continuous System Modeling. Springer (1991). https:\/\/doi.org\/10.1007\/978-1-4757-3922-0","DOI":"10.1007\/978-1-4757-3922-0"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Chen, J., et al.: Synchronous programming with refinement types. Proc. ACM Program. Lang. 8(ICFP), 268:938\u2013268:972 (2024). https:\/\/doi.org\/10.1145\/3674657","DOI":"10.1145\/3674657"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Cola\u00e7o, J.L., Pagano, B., Pouzet, M.: Scade 6: a formal language for embedded critical software development (invited paper). In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1\u201311. IEEE (2017). https:\/\/doi.org\/10.1109\/TASE.2017.8285623","DOI":"10.1109\/TASE.2017.8285623"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Fulton, N., Mitsch, S., Quesel, J.D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: International Conference on Automated Deduction, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 278\u2013292. IEEE (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561342","DOI":"10.1109\/LICS.1996.561342"},{"issue":"3\u20134","key":"21_CR15","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1561\/2500000032","volume":"6","author":"R Jhala","year":"2021","unstructured":"Jhala, R., Vazou, N.: Refinement types: a tutorial. Found. Trends Program. Lang. 6(3\u20134), 159\u2013317 (2021). https:\/\/doi.org\/10.1561\/2500000032","journal-title":"Found. Trends Program. Lang."},{"issue":"2","key":"21_CR16","first-page":"04-1","volume":"8","author":"E Kamburjan","year":"2022","unstructured":"Kamburjan, E., Mitsch, S., H\u00e4hnle, R.: A hybrid programming language for formal modeling and verification of hybrid systems. Leibniz Trans. Embed. Syst. 8(2), 04\u20131 (2022)","journal-title":"Leibniz Trans. Embed. Syst."},{"key":"21_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.nahs.2015.10.004","volume":"20","author":"M Kone\u010dn\u00fd","year":"2016","unstructured":"Kone\u010dn\u00fd, M., Taha, W., Bartha, F., Duracz, J., Duracz, A., Ames, A.: Enclosing the behavior of a hybrid automaton up to and beyond a zeno point. Nonlinear Anal. Hybrid Syst 20, 1\u201320 (2016). https:\/\/doi.org\/10.1016\/j.nahs.2015.10.004","journal-title":"Nonlinear Anal. Hybrid Syst"},{"issue":"9","key":"21_CR18","doi-asserted-by":"publisher","first-page":"1321","DOI":"10.1109\/5.97301","volume":"79","author":"P Le Guernic","year":"1991","unstructured":"Le Guernic, P., Gautier, T., Le Borgne, M., Le Maire, C.: Programming real-time applications with SIGNAL. Proc. IEEE 79(9), 1321\u20131336 (1991). https:\/\/doi.org\/10.1109\/5.97301","journal-title":"Proc. IEEE"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Hybrid Systems: Computation and Control (HSCC 2005). Lecture Notes in Computer Science, vol.\u00a03414, pp. 25\u201353 (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_2","DOI":"10.1007\/978-3-540-31954-2_2"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Lin, S., et al.: Towards building verifiable CPS using lingua franca. ACM Trans. Embed. Comput. Syst. 22(5s), 155:1\u2013155:24 (2023). https:\/\/doi.org\/10.1145\/3609134","DOI":"10.1145\/3609134"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM 2011: Formal Methods. Lecture Notes in Computer Science, vol.\u00a06664, pp. 42\u201356. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_6","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Marin, M., \u00d6lveczky, P.C., Reja, M., Rukhaia, M., Bae, K., Dundua, B.: Semantics and formal analysis of lingua franca CPS specifications in rewriting logic. Tech. rep., University of Oslo \/ Collaborators (technical Report) (2024)","DOI":"10.1007\/978-3-031-85134-6_4"},{"issue":"5\u20136","key":"21_CR23","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5\u20136), 865\u2013911 (2008). https:\/\/doi.org\/10.1017\/S0956796808006953","journal-title":"J. Funct. Program."},{"issue":"2","key":"21_CR24","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reason."},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0","DOI":"10.1007\/978-3-319-63588-0"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Hybrid Systems: Computation and Control. HSCC 2004. Lecture Notes in Computer Science, pp. 477\u2013492. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 159\u2013169 (2008). https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"21_CR28","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: Liquid haskell: experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, pp. 39\u201351 (2014). https:\/\/doi.org\/10.1145\/2633357.2633366","DOI":"10.1145\/2633357.2633366"},{"key":"21_CR29","doi-asserted-by":"publisher","unstructured":"White, L., Titolo, L., Slagel, J.T., Mu\u00f1oz, C.: A temporal differential dynamic logic formal embedding. In: CPP 2024, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 162\u2013176. Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3636501.3636943","DOI":"10.1145\/3636501.3636943"},{"issue":"1","key":"21_CR30","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1093","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:31:59Z","timestamp":1781191919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}