{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:31:58Z","timestamp":1777890718509,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031274800","type":"print"},{"value":"9783031274817","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-27481-7_11","type":"book-chapter","created":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T14:03:10Z","timestamp":1677765790000},"page":"160-178","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["HHLPy: Practical Verification of\u00a0Hybrid Systems Using Hoare Logic"],"prefix":"10.1007","author":[{"given":"Huanhuan","family":"Sheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Bentkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) Conference on Certified Programs and Proofs (CPP 2017), pp. 208\u2013221. ACM (2017)","DOI":"10.1145\/3018610.3018616"},{"key":"11_CR2","series-title":"NASA Monographs in Systems and Software Engineering","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-48628-4_3","volume-title":"Provably Correct Systems","author":"M Chen","year":"2017","unstructured":"Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 39\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-48628-4_3"},{"issue":"8","key":"11_CR3","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"11_CR4","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-90870-6_20","volume-title":"Formal Methods","author":"S Foster","year":"2021","unstructured":"Foster, S., Huerta y Munive, J.J., Gleirscher, M., Struth, G.: Hybrid systems verification with Isabelle\/HOL: simpler syntax, better models, faster proofs. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 367\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_20"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-030-43520-2_11","volume-title":"Relational and Algebraic Methods in Computer Science","author":"S Foster","year":"2020","unstructured":"Foster, S., Huerta y Munive, J.J., Struth, G.: Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds.) RAMiCS 2020. LNCS, vol. 12062, pp. 169\u2013186. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_11"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-66107-0_14","volume-title":"Interactive Theorem Proving","author":"N Fulton","year":"2017","unstructured":"Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: tactical theorem proving for\u00a0hybrid systems. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 207\u2013224. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_14"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Neves, R.: An adequate while-language for hybrid computation. In: Komendantskaya, E. (ed.) International Symposium on Principles and Practice of Programming Languages (PPDP 2019), pp. 11:1\u201311:15. ACM (2019)","DOI":"10.1145\/3354166.3354176"},{"key":"11_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2022.102665","volume":"130","author":"P Guo","year":"2022","unstructured":"Guo, P., Zhan, B., Xu, X., Wang, S., Sun, W.: Translating a large subset of Stateflow to hybrid CSP with code optimization. J. Syst. Archit. 130, 102665 (2022)","journal-title":"J. Syst. Archit."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"11_CR13","unstructured":"Jifeng, H.: From CSP to hybrid systems, pp. 171\u2013189. Prentice Hall International (UK) Ltd., GBR (1994)"},{"key":"11_CR14","unstructured":"Kekatos, N.: Verifying a cruise control system using Simulink and SpaceEx. CoRR abs\/2101.00102 (2021)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-030-02450-5_6","volume-title":"Formal Methods and Software Engineering","author":"T Liebrenz","year":"2018","unstructured":"Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89\u2013105. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_6"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Jin, X., Zhan, B., Wang, S., Zhan, N.: ARCH-COMP21 category report: hybrid systems theorem proving. In: Frehse, G., Althoff, M. (eds.) International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2021). EPiC Series in Computing, vol. 80, pp. 120\u2013132. EasyChair (2021)","DOI":"10.29007\/35cf"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-030-58768-0_5","volume-title":"Software Engineering and Formal Methods","author":"JJ Huerta y Munive","year":"2020","unstructured":"Huerta y Munive, J.J.: Affine systems of ODEs in Isabelle\/HOL for hybrid-program verification. In: de Boer, F., Cerone, A. (eds.) SEFM 2020. LNCS, vol. 12310, pp. 77\u201392. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_5"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-030-02149-8_14","volume-title":"Relational and Algebraic Methods in Computer Science","author":"JJ Huerta y Munive","year":"2018","unstructured":"Huerta y Munive, J.J., Struth, G.: Verifying hybrid systems with modal Kleene algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) RAMiCS 2018. LNCS, vol. 11194, pp. 225\u2013243. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02149-8_14"},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10817-021-09607-x","volume":"66","author":"JJ Huerta\u00a0y\u00a0Munive","year":"2021","unstructured":"Huerta\u00a0y\u00a0Munive, J.J., Struth, G.: Predicate transformer semantics for hybrid systems. J. Autom. Reason. 66(1), 93\u2013139 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09607-x","journal-title":"J. Autom. Reason."},{"issue":"2","key":"11_CR23","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)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219\u2013265 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reason."},{"key":"11_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical Foundations of Cyber-Physical Systems","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM 67(1), 6:1\u20136:66 (2020)","DOI":"10.1145\/3380825"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: practical verification of hybrid systems using Hoare logic (full paper). CoRR abs\/2210.17163 (2022). https:\/\/doi.org\/10.48550\/arXiv.2210.17163","DOI":"10.48550\/arXiv.2210.17163"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"key":"11_CR30","unstructured":"Wolfram Research Inc.: Wolfram Engine, Version 13.1, Champaign, IL (2022). https:\/\/www.wolfram.com\/engine"},{"key":"11_CR31","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100809","volume":"130","author":"X Xu","year":"2023","unstructured":"Xu, X., Zhan, B., Wang, S., Talpin, J.P., Zhan, N.: A denotational semantics of Simulink with higher-order UTP. J. Log. Algebraic Methods Program. 130, 100809 (2023)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"11_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47016-0","volume-title":"Formal Verification of Simulink\/Stateflow Diagrams","author":"N Zhan","year":"2017","unstructured":"Zhan, N., Wang, S., Zhao, H.: Formal Verification of Simulink\/Stateflow Diagrams. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-47016-0"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/BFb0020972","volume-title":"Hybrid Systems III","author":"Z Chaochen","year":"1996","unstructured":"Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511\u2013530. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020972"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-24953-7_33","volume-title":"Automated Technology for Verification and Analysis","author":"L Zou","year":"2015","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M.: Formal verification of Simulink\/Stateflow diagrams. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 464\u2013481. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_33"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid Hoare logic prover. In: Ernst, R., Sokolsky, O. (eds.) International Conference on Embedded Software, (EMSOFT 2013), pp. 9:1\u20139:10. IEEE (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-27481-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,15]],"date-time":"2024-10-15T16:22:27Z","timestamp":1729009347000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-27481-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031274800","9783031274817"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-27481-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 March 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"L\u00fcbeck","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 March 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 March 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fm2023.isp.uni-luebeck.de\/wordpress\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"95","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also include 7 short industry papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}