{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:31:57Z","timestamp":1777890717650,"version":"3.51.4"},"reference-count":78,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T00:00:00Z","timestamp":1729296000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T00:00:00Z","timestamp":1729296000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"name":"Novo Nordisk Fonden Start Package Grant","award":["NNF20OC0063462"],"award-info":[{"award-number":["NNF20OC0063462"]}]},{"name":"Horizon MSCA 2022 Postdoctoral Fellowship","award":["101102608"],"award-info":[{"award-number":["101102608"]}]},{"name":"UKRI-EPSRC project CyPhyAssure","award":["EP\/S001190\/1"],"award-info":[{"award-number":["EP\/S001190\/1"]}]},{"name":"Assuring Autonomy International Programme","award":["CSI:Cobot"],"award-info":[{"award-number":["CSI:Cobot"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10817-024-09709-2","type":"journal-article","created":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T10:02:10Z","timestamp":1729332130000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale"],"prefix":"10.1007","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3279-3685","authenticated-orcid":false,"given":"Jonathan Juli\u00e1n","family":"Huerta y Munive","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-9514","authenticated-orcid":false,"given":"Simon","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9445-6863","authenticated-orcid":false,"given":"Mario","family":"Gleirscher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9466-7815","authenticated-orcid":false,"given":"Georg","family":"Struth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7838-2764","authenticated-orcid":false,"given":"Christian","family":"Pardillo\u00a0Laursen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7216-1696","authenticated-orcid":false,"given":"Thomas","family":"Hickman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,19]]},"reference":[{"key":"9709_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m-Mumm, E., Steffen, M., Hannemann, U.: Verification of hybrid systems: formalization and proof rules in PVS. In: ICECCS 2001, pp. 48\u201357. IEEE Computer Society, New Jersey (2001)","DOI":"10.1109\/ICECCS.2001.930163"},{"issue":"5","key":"9709_CR2","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF02477259","volume":"27","author":"E Ackerman","year":"1965","unstructured":"Ackerman, E., Gatewood, L.C., Rosevear, J.W., Molnar, G.D.: Model studies of blood-glucose regulation. Bull. Math. Biophys. 27(5), 21\u201337 (1965). https:\/\/doi.org\/10.1007\/BF02477259","journal-title":"Bull. Math. Biophys."},{"issue":"2","key":"9709_CR3","doi-asserted-by":"publisher","first-page":"01","DOI":"10.4230\/LITES.8.2.1","volume":"8","author":"AS Adimoolam","year":"2022","unstructured":"Adimoolam, A.S., Dang, T.: Safety verification of networked control systems by complex zonotopes. Leibniz Trans. Embed. Syst. 8(2), 01\u201310122 (2022). https:\/\/doi.org\/10.4230\/LITES.8.2.1","journal-title":"Leibniz Trans. Embed. Syst."},{"issue":"3","key":"9709_CR4","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/S10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010). https:\/\/doi.org\/10.1007\/S10817-009-9149-2","journal-title":"J. Autom. Reason."},{"key":"9709_CR5","doi-asserted-by":"publisher","unstructured":"Althoff, M.: An introduction to CORA 2015. In: ARCH 2015, vol. 34, pp. 120\u2013151. EasyChair, EasyChair (2015). https:\/\/doi.org\/10.29007\/zbkv","DOI":"10.29007\/zbkv"},{"key":"9709_CR6","doi-asserted-by":"crossref","unstructured":"Anand, A., Knepper, R.A.: Roscoq: robots powered by constructive reals. In: ITP. LNCS, vol. 9236, pp. 34\u201350. Springer, Heidelberg (2015)","DOI":"10.1007\/978-3-319-22102-1_3"},{"issue":"2","key":"9709_CR7","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s00165-015-0343-1","volume":"28","author":"A Armstrong","year":"2016","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Building program construction and verification tools from algebraic principles. Formal Aspects Comput. 28(2), 265\u2013293 (2016)","journal-title":"Formal Aspects Comput."},{"key":"9709_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus\u2014A Systematic Introduction","author":"R Back","year":"1998","unstructured":"Back, R., Wright, J.: Refinement Calculus\u2014A Systematic Introduction. Springer, Heidelberg (1998)"},{"key":"9709_CR9","doi-asserted-by":"publisher","DOI":"10.1145\/3625563","author":"J Baxter","year":"2023","unstructured":"Baxter, J., Carvalho, G., Cavalcanti, A., J\u00fanior, F.R.: Roboworld: verification of robotic systems with environment in the loop. Formal Aspects Comput. (2023). https:\/\/doi.org\/10.1145\/3625563. (Just Accepted)","journal-title":"Formal Aspects Comput."},{"key":"9709_CR10","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1) (2016)"},{"key":"9709_CR11","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Ozay, N., Prabhakar, P. (eds.) HSCC 2019, pp. 39\u201344. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3302504.3311804","DOI":"10.1145\/3302504.3311804"},{"key":"9709_CR12","doi-asserted-by":"crossref","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: CPP, pp. 208\u2013221. ACM, New York (2017)","DOI":"10.1145\/3018610.3018616"},{"issue":"5s","key":"9709_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3477024","volume":"20","author":"R Bohrer","year":"2021","unstructured":"Bohrer, R., Platzer, A.: Structured proofs for adversarial cyber-physical systems. ACM Trans. Embed. Comput. Syst. 20(5s), 1\u201326 (2021). https:\/\/doi.org\/10.1145\/3477024","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"9709_CR14","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: BACH 2 : bounded reachability checker for compositional linear hybrid systems. In: DATE 2010, pp. 1512\u20131517. IEEE Computer Society, New Jersey (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"9709_CR15","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A., Attala, Z., Baxter, J., Miyazawa, A., Ribeiro, P.: Model-based engineering for robotics with RoboChart and RoboTool, pp. 106\u2013151. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-43678-9_4","DOI":"10.1007\/978-3-031-43678-9_4"},{"key":"9709_CR16","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"9709_CR17","unstructured":"Cordwell, K., Yong, K.T., A., P.: A verified decision procedure for univariate real arithmetic with the BKR algorithm. In: Cohen, L., Kaliszyk, C. (eds.) ITP. Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 14-11420. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Germany (2021)"},{"key":"9709_CR18","doi-asserted-by":"crossref","unstructured":"Foster, S., Baxter, J.: Automated algebraic reasoning for collections and local variables with lenses. In: RAMiCS. LNCS, vol. 12062. Springer, Heidelberg (2020)","DOI":"10.1007\/978-3-030-43520-2_7"},{"key":"9709_CR19","doi-asserted-by":"crossref","unstructured":"Foster, S., Gleirscher, M., Calinescu, R.: Towards deductive verification of control algorithms for autonomous marine vehicles. In: ICECCS. IEEE, New Jersey (2020)","DOI":"10.1109\/ICECCS51672.2020.00020"},{"key":"9709_CR20","doi-asserted-by":"publisher","unstructured":"Foster, S., Huerta y Munive, J.J., Struth, G.: Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL. In: RAMiCS[postponed]. LNCS, vol. 12062, pp. 169\u2013186 (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_11","DOI":"10.1007\/978-3-030-43520-2_11"},{"key":"9709_CR21","doi-asserted-by":"publisher","unstructured":"Foster, S., Munive, J.J.H., Gleirscher, M., Struth, G.: Hybrid systems verification with Isabelle\/HOL: simpler syntax, better models, faster proofs. In: FM 2021. LNCS, vol. 13047, pp. 367\u2013386. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_20","DOI":"10.1007\/978-3-030-90870-6_20"},{"key":"9709_CR22","doi-asserted-by":"crossref","unstructured":"Foster, S., Nemouchi, Y., Gleirscher, M., Wei, R., Kelly, T.: Integration of formal proof into unified assurance cases with Isabelle\/SACM. Formal Aspects Comput. (2021)","DOI":"10.1007\/s00165-021-00537-4"},{"key":"9709_CR23","unstructured":"Foster, S., Zeyda, F.: Optics. Archive of Formal Proofs (2017)"},{"key":"9709_CR24","unstructured":"Foster, J.: Bidirectional programming languages. PhD thesis, University of Pennsylvania (2009)"},{"key":"9709_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102510","volume":"197","author":"S Foster","year":"2020","unstructured":"Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying semantic foundations for automated verification tools in Isabelle\/UTP. Sci. Comput. Programm. 197, 102510 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102510","journal-title":"Sci. Comput. Programm."},{"key":"9709_CR26","doi-asserted-by":"crossref","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"9709_CR27","doi-asserted-by":"publisher","unstructured":"Frehse, G., Krogh, B.H., Rutenbar, R.A., Maler, O.: Time domain verification of oscillator circuit properties. In: Maler, O. (ed.) FAC 2005. ENTCS, vol. 153, pp. 9\u201322. Elsevier, Amsterdam (2005). https:\/\/doi.org\/10.1016\/j.entcs.2006.02.019","DOI":"10.1016\/j.entcs.2006.02.019"},{"key":"9709_CR28","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: Felty, A.P., Middeldorp, A. (eds.) CADE. LNCS, vol. 9195, pp. 527\u2013538. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"9709_CR29","doi-asserted-by":"publisher","unstructured":"Gallicchio, J., Tan, Y.K., Mitsch, S., Platzer, A.: Implicit definitions with differential equations for keymaera X\u2014(system description). In: IJCAR 2022, pp. 723\u2013733 (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_42","DOI":"10.1007\/978-3-031-10769-6_42"},{"key":"9709_CR30","doi-asserted-by":"crossref","unstructured":"Gomes, V.B.F., Struth, G.: Modal Kleene algebra applied to program correctness. In: FM. LNCS, vol. 9995, pp. 310\u2013325 (2016)","DOI":"10.1007\/978-3-319-48989-6_19"},{"key":"9709_CR31","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"9709_CR32","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: ITP. LNCS, vol. 7998, pp. 279\u2013294. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_21","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"9709_CR33","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: PLMMS, pp. 38\u201345. ACM, New York (2009)"},{"key":"9709_CR34","doi-asserted-by":"publisher","unstructured":"Huerta y Munive, J.J.: Affine systems of ODEs in Isabelle\/HOL for hybrid-program verification. In: SEFM. LNCS, vol. 12310, pp. 77\u201392. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_5","DOI":"10.1007\/978-3-030-58768-0_5"},{"key":"9709_CR35","unstructured":"Immler, F., H\u00f6lzl, J.: Ordinary differential equations. Archive of Formal Proofs (2012)"},{"key":"9709_CR36","doi-asserted-by":"publisher","unstructured":"Immler, F., Traut, C.: The flow of ODEs: Formalization of variational equation and poincar\u00e9. In: ITP 2016. LNCS, vol. 9807, pp. 184\u2013199. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/s10817-018-9449-5","DOI":"10.1007\/s10817-018-9449-5"},{"issue":"2","key":"9709_CR37","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10817-018-9449-5","volume":"62","author":"F Immler","year":"2019","unstructured":"Immler, F., Traut, C.: The flow of ODEs: formalization of variational equation and Poincar\u00e9 map. J. Autom. Reason. 62(2), 215\u2013236 (2019)","journal-title":"J. Autom. Reason."},{"issue":"6","key":"9709_CR38","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1007\/s10009-016-0434-1","volume":"19","author":"J Jeannin","year":"2017","unstructured":"Jeannin, J., Ghorbal, K., Kouskoulas, Y., Schmidt, A., Gardner, R., Mitsch, S., Platzer, A.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT 19(6), 717\u2013741 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0434-1","journal-title":"STTT"},{"key":"9709_CR39","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10817-018-9454-8","volume":"62","author":"O Kuncar","year":"2019","unstructured":"Kuncar, O., Popescu, A.: A consistent foundation for Isabelle\/HOL. J. Autom. Reason. 62, 531\u2013555 (2019)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9709_CR40","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10817-017-9437-1","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Refinement to imperative HOL. J. Autom. Reason. 62(4), 481\u2013503 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9437-1","journal-title":"J. Autom. Reason."},{"key":"9709_CR41","doi-asserted-by":"publisher","unstructured":"Li, Y., Zhu, H., Braught, K., Shen, K., Mitra, S.: Verse: A python library for reasoning about multi-agent hybrid system scenarios. In: CAV 2023. LNCS, vol. 13964, pp. 351\u2013364. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_18","DOI":"10.1007\/978-3-031-37706-8_18"},{"key":"9709_CR42","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/s10817-017-9424-6","volume":"62","author":"W Li","year":"2019","unstructured":"Li, W., Passmore, G., Paulson, L.: Deciding univariate polynomial problems using untrusted certificates in Isabelle\/HOL. J. Autom. Reason. 62, 29\u201391 (2019)","journal-title":"J. Autom. Reason."},{"key":"9709_CR43","doi-asserted-by":"publisher","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: FM 2011. LNCS, vol. 6664, pp. 42\u201356. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_6","DOI":"10.1007\/978-3-642-21437-0_6"},{"issue":"3","key":"9709_CR44","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T.C., Wenzel, M.: Eisbach: a proof method language for Isabelle. J. Autom. Reason. 56(3), 261\u2013282 (2016)","journal-title":"J. Autom. Reason."},{"key":"9709_CR45","doi-asserted-by":"publisher","unstructured":"Mitsch, S., Huerta y Munive, J.J., Jin, X., Zhan, B., Wang, S., Zhan, N.: ARCH-COMP20 category report: hybrid systems theorem proving. In: ARCH20., vol. 74, pp. 141\u2013161. EasyChair, EasyChair (2020). https:\/\/doi.org\/10.29007\/bdq9","DOI":"10.29007\/bdq9"},{"key":"9709_CR46","unstructured":"Mitsch, S., Platzer, A.: Verified runtime validation for partially observable hybrid systems. (2018). arXiv:1811.06502"},{"key":"9709_CR47","doi-asserted-by":"publisher","unstructured":"Mitsch, S., Zhan, B., Sheng, H., Bentkamp, A., Jin, X., Wang, S., Foster, S., Laursen, C.P., Munive, J.J.H.: ARCH-COMP22 category report: hybrid systems theorem proving. In: ARCH22. EPiC Series in Computing, vol. 90, pp. 185\u2013203. EasyChair, Munich (2022). https:\/\/doi.org\/10.29007\/4lxf","DOI":"10.29007\/4lxf"},{"key":"9709_CR48","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18, 3097\u20133149 (2019)","journal-title":"Softw. Syst. Model."},{"key":"9709_CR49","unstructured":"Munive, J.J.: Algebraic verification of hybrid systems in Isabelle\/HOL. PhD thesis, The University of Sheffield (2021)"},{"issue":"1","key":"9709_CR50","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10817-021-09607-x","volume":"66","author":"JJ Munive","year":"2022","unstructured":"Munive, J.J., Struth, G.: Predicate transformer semantics for hybrid systems. J. Autom. Reason. 66(1), 93\u2013139 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09607-x","journal-title":"J. Autom. Reason."},{"key":"9709_CR51","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. In: Proc. ACM Program. Lang. 4(POPL), 10-11032 (2020). https:\/\/doi.org\/10.1145\/3371078","DOI":"10.1145\/3371078"},{"key":"9709_CR52","unstructured":"Oles, F.: A category-theoretic approach to the semantics of programming languages. PhD thesis, Syracuse University (1982)"},{"key":"9709_CR53","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010. EPiC Series in Computing, vol. 2, pp. 1\u201311. EasyChair, EasyChair (2010). https:\/\/doi.org\/10.29007\/36dt","DOI":"10.29007\/36dt"},{"key":"9709_CR54","doi-asserted-by":"crossref","unstructured":"Platzer, A., Quesel, J.: European train control system: a case study in formal verification. In: ICFEM. LNCS, vol. 5885, pp. 246\u2013265. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-10373-5_13"},{"key":"9709_CR55","doi-asserted-by":"crossref","unstructured":"Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: LICS, pp. 819\u2013828. ACM, New Jersey (2018)","DOI":"10.1145\/3209108.3209147"},{"key":"9709_CR56","unstructured":"Platzer, A.: Differential game logic. Archive of Formal Proofs (2019)"},{"key":"9709_CR57","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13\u201324 (2012). https:\/\/doi.org\/10.1109\/LICS.2012.13","DOI":"10.1109\/LICS.2012.13"},{"key":"9709_CR58","doi-asserted-by":"crossref","unstructured":"Platzer, A.: The structure of differential invariants and differential cut elimination. Logical Methods Comput. Sci. 8(4) (2008)","DOI":"10.2168\/LMCS-8(4:16)2012"},{"key":"9709_CR59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems. Springer, Heidelberg (2010)"},{"issue":"1","key":"9709_CR60","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2817824","volume":"17","author":"A Platzer","year":"2015","unstructured":"Platzer, A.: Differential game logic. ACM TOCL 17(1), 1\u20131152 (2015)","journal-title":"ACM TOCL"},{"key":"9709_CR61","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, Heidelberg (2018)"},{"issue":"1","key":"9709_CR62","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"J Quesel","year":"2016","unstructured":"Quesel, J., Mitsch, S., Loos, S.M., Arechiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transf. 18(1), 67\u201391 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9709_CR63","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS. IEEE, New Jersey (2002)"},{"key":"9709_CR64","doi-asserted-by":"crossref","unstructured":"Ricketts, D., Malecha, G., Alvarez, M.M., Gowda, V., Lerner, S.: Towards verification of hybrid systems in a foundational proof assistant. In: MEMOCODE, pp. 248\u2013257. IEEE, New Jersey (2015)","DOI":"10.1109\/MEMCOD.2015.7340492"},{"key":"9709_CR65","doi-asserted-by":"publisher","unstructured":"Scharager, M., Cordwell, K., Mitsch, S., Platzer, A.: Verified quadratic virtual substitution for real arithmetic. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 200\u2013217. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_11","DOI":"10.1007\/978-3-030-90870-6_11"},{"key":"9709_CR66","doi-asserted-by":"crossref","unstructured":"Schirmer, N., Wenzel, M.: State spaces\u2014the locale way. In: SSV 2009. ENTCS, vol. 254, pp. 161\u2013179 (2009)","DOI":"10.1016\/j.entcs.2009.09.065"},{"key":"9709_CR67","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in isabelle-hol. PhD thesis, Technical University Munich, Germany (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9709_CR68","doi-asserted-by":"publisher","unstructured":"Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: practical verification of hybrid systems using hoare logic. In: Chechik, M., Katoen, J., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 160\u2013178. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_11","DOI":"10.1007\/978-3-031-27481-7_11"},{"issue":"5","key":"9709_CR69","doi-asserted-by":"publisher","first-page":"885","DOI":"10.1016\/j.mcm.2009.05.017","volume":"50","author":"D Stanescu","year":"2009","unstructured":"Stanescu, D., Chen-Charpentier, B.M.: Random coefficient differential equation models for bacterial growth. Math. Comput. Model. 50(5), 885\u2013895 (2009). https:\/\/doi.org\/10.1016\/j.mcm.2009.05.017","journal-title":"Math. Comput. Model."},{"key":"9709_CR70","unstructured":"Struth, G.: Transformer semantics. Archive of Formal Proofs (2018)"},{"key":"9709_CR71","doi-asserted-by":"publisher","DOI":"10.1090\/gsm\/140","volume-title":"Ordinary Differential Equations and Dynamical Systems","author":"G Teschl","year":"2012","unstructured":"Teschl, G.: Ordinary Differential Equations and Dynamical Systems. AMS, Rhode Island (2012)"},{"key":"9709_CR72","unstructured":"The Sage Developers: SageMath, the Sage Mathematics Software System (Version 9.0). (2020)"},{"key":"9709_CR73","doi-asserted-by":"crossref","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: ICFEM. LNCS, vol. 9407, pp. 382\u2013399 (2015)","DOI":"10.1007\/978-3-319-25423-4_25"},{"key":"9709_CR74","doi-asserted-by":"publisher","unstructured":"Weinert, F.: Radioactive Decay Law (Rutherford\u2013Soddy), pp. 630\u2013632. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-540-70626-7_183","DOI":"10.1007\/978-3-540-70626-7_183"},{"key":"9709_CR75","unstructured":"Wolfram Research: Expressions\u2014Wolfram Language. https:\/\/reference.wolfram.com\/language\/guide\/Expressions.html. Accessed 11 Jan 2024"},{"key":"9709_CR76","unstructured":"Wolfram Research: Wolfram Engine. https:\/\/www.wolfram.com\/engine\/. Accessed 05 Jan 2024"},{"key":"9709_CR77","doi-asserted-by":"publisher","unstructured":"Xiang, J., Fulton, N., Chong, S.: Relational analysis of sensor attacks on cyber-physical systems. In: CSF 2021, pp. 1\u201316. IEEE, New Jersey (2021). https:\/\/doi.org\/10.1109\/CSF51468.2021.00035","DOI":"10.1109\/CSF51468.2021.00035"},{"key":"9709_CR78","doi-asserted-by":"publisher","unstructured":"Zhan, N., Zhan, B., Wang, S., Guelev, D.P., Jin, X.: A generalized hybrid Hoare logic. CoRR arXiv:2303.15020 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.15020","DOI":"10.48550\/arXiv.2303.15020"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09709-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09709-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09709-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,14]],"date-time":"2024-12-14T07:07:17Z","timestamp":1734160037000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09709-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,19]]},"references-count":78,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["9709"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09709-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,19]]},"assertion":[{"value":"17 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 October 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"21"}}