{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T11:05:41Z","timestamp":1772795141027,"version":"3.50.1"},"reference-count":76,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,2,18]],"date-time":"2026-02-18T00:00:00Z","timestamp":1771372800000},"content-version":"vor","delay-in-days":17,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"DOI":"10.13039\/501100005366","name":"University of Oslo","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005366","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1007\/s10703-026-00491-y","type":"journal-article","created":{"date-parts":[[2026,2,18]],"date-time":"2026-02-18T16:35:25Z","timestamp":1771432525000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Modular analysis of distributed hybrid systems using post-regions"],"prefix":"10.1007","volume":"68","author":[{"given":"Eduard","family":"Kamburjan","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,2,18]]},"reference":[{"key":"491_CR1","doi-asserted-by":"publisher","unstructured":"Platzer A (2010) Differential-algebraic dynamic logic for differential-algebraic programs. J Log Computation 20(1). https:\/\/doi.org\/10.1093\/LOGCOM\/EXN070","DOI":"10.1093\/LOGCOM\/EXN070"},{"key":"491_CR2","doi-asserted-by":"publisher","unstructured":"Platzer A (2012) A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. LMCS 8(4). https:\/\/doi.org\/10.2168\/LMCS-8(4:17)2012","DOI":"10.2168\/LMCS-8(4:17)2012"},{"key":"491_CR3","doi-asserted-by":"publisher","unstructured":"Ahrendt W, Beckert B, Bubel R (eds, et al (2016) Deductive software verification - the KeY book - from theory to practice, LNCS, vol 10001. Springer. https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"491_CR4","doi-asserted-by":"publisher","unstructured":"Meyer B (1992) Applying \u201cdesign by contract\u201d. IEEE Comput 25(10). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"491_CR5","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D Harel","year":"2000","unstructured":"Harel D, Tiuryn J, Kozen D (2000) Dynamic logic. MIT Press. https:\/\/mitpress.mit.edu\/9780262527668\/dynamic-logic\/"},{"key":"491_CR6","doi-asserted-by":"publisher","unstructured":"Platzer A (2012) The complete proof theory of hybrid systems. In LICS, IEEE. https:\/\/doi.org\/10.1109\/LICS.2012.64","DOI":"10.1109\/LICS.2012.64"},{"key":"491_CR7","unstructured":"Kamburjan E, Mitsch S, Kettenbach M et al. (2019) Modeling and verifying cyber-physical systems with hybrid active objects. CoRR Abs\/1906.05704. http:\/\/arxiv.org\/abs\/1906.05704"},{"key":"491_CR8","doi-asserted-by":"publisher","unstructured":"Kamburjan E, Mitsch S, H\u00e4hnle R (2022) A hybrid programming language for formal modeling and verification of hybrid systems. Leibniz Trans Embed Syst 8(2). https:\/\/doi.org\/10.4230\/LITES.8.2.4","DOI":"10.4230\/LITES.8.2.4"},{"key":"491_CR9","doi-asserted-by":"crossref","unstructured":"de Boer FS, Serbanescu V, H\u00e4hnle R et al. (2017) A survey of active object languages. ACM Comput Surv 50(5)","DOI":"10.1145\/3122848"},{"key":"491_CR10","doi-asserted-by":"publisher","unstructured":"Albert E, de Boer FS, H\u00e4hnle R et al. (2014) Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Serv Oriented Comput Appl 8(4). https:\/\/doi.org\/10.1007\/S11761-013-0148-0","DOI":"10.1007\/S11761-013-0148-0"},{"key":"491_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_20","volume-title":"FASE, LNCS","author":"N Bezirgiannis","year":"2019","unstructured":"Bezirgiannis N, de Boer FS, Johnsen EB et al. (2019) Implementing SOS with active objects: a case study of a multicore memory system. In: H\u00e4hnle R, van der Aalst WMP (eds) FASE, LNCS, vol 11424. Springer. https:\/\/doi.org\/10.1007\/978-3-030-16722-6_20"},{"key":"491_CR12","doi-asserted-by":"publisher","unstructured":"Kamburjan E, H\u00e4hnle R, Sch\u00f6n S (2018) Formal modeling and analysis of railway operations with active objects. Sci Comput Program 166. https:\/\/doi.org\/10.1016\/j.scico.2018.07.001","DOI":"10.1016\/j.scico.2018.07.001"},{"key":"491_CR13","doi-asserted-by":"publisher","unstructured":"Lin J, Lee M, Yu IC et al. (2020) A configurable and executable model of spark streaming on apache YARN. Int J Grid Util Comput 11(2). https:\/\/doi.org\/10.1504\/IJGUC.2020.105531","DOI":"10.1504\/IJGUC.2020.105531"},{"key":"491_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68499-4_9","volume-title":"Rssrail, LNCS","author":"E Kamburjan","year":"2017","unstructured":"Kamburjan E, H\u00e4hnle R (2017) Deductive verification of railway operations. In: Fantechi A, Lecomte T, Romanovsky AB (eds) Rssrail, LNCS, vol 10598. Springer. https:\/\/doi.org\/10.1007\/978-3-319-68499-4_9"},{"key":"491_CR15","doi-asserted-by":"publisher","unstructured":"Flanagan C, Felleisen M (1999) The semantics of future and an application. J Funct Program 9(1). https:\/\/doi.org\/10.1017\/s0956796899003329","DOI":"10.1017\/s0956796899003329"},{"key":"491_CR16","doi-asserted-by":"publisher","unstructured":"Halstead JRH (1985) Multilisp: a language for concurrent symbolic computation. ACM Trans Program Lang Syst 7(4). https:\/\/doi.org\/10.1145\/4472.4478","DOI":"10.1145\/4472.4478"},{"key":"491_CR17","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354176","volume-title":"PPDP","author":"S Goncharov","year":"2019","unstructured":"Goncharov S, Neves R (2019) An adequate while-language for hybrid computation. In: Komendantskaya E (ed) PPDP. ACM. https:\/\/doi.org\/10.1145\/3354166.3354176"},{"key":"491_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-23703-5_1","volume-title":"CyPhy, LNCS","author":"I Jahandideh","year":"2018","unstructured":"Jahandideh I, Ghassemi F, Sirjani M (2018) Hybrid rebeca: modeling and analyzing of cyber-physical systems. In: Chamberlain RD, Taha W, T\u00f6rngren M (eds) CyPhy, LNCS, vol 11615. Springer. https:\/\/doi.org\/10.1007\/978-3-030-23703-5_1"},{"key":"491_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_31","volume-title":"ICALP (2), LNCS","author":"K Suenaga","year":"2011","unstructured":"Suenaga K, Hasuo I (2011) Programming with infinitesimals: a while-language f or hybrid system modeling. In: ICALP (2), LNCS, vol 6756. Springer. https:\/\/doi.org\/10.1007\/978-3-642-22012-8_31"},{"key":"491_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-8_6","volume-title":"CADE, LNCS","author":"M Brieger","year":"2023","unstructured":"Brieger M, Mitsch S, Platzer A (2023) Uniform substitution for dynamic logic with communicating hybrid programs. In: Pientka B, Tinelli C (eds) CADE, LNCS, vol 14132. Springer. https:\/\/doi.org\/10.1007\/978-3-031-38499-8_6"},{"key":"491_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"ICFEM","author":"S Wang","year":"2015","unstructured":"Wang S, Zhan N, Zou L (2015) An improved HHL prover: an interactive theorem prover for hybrid systems. In: ICFEM. Springer. https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"key":"491_CR22","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456633","volume-title":"HSCC","author":"E Kamburjan","year":"2021","unstructured":"Kamburjan E (2021) From post-conditions to post-region invariants: deductive verification of hybrid objects. In: Bogomolov S, Jungers RM (eds) HSCC. ACM. https:\/\/doi.org\/10.1145\/3447928.3456633"},{"key":"491_CR23","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 (2018) Logical foundations of cyber-physical systems. Springer. https:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"491_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"CADE, LNCS","author":"N Fulton","year":"2015","unstructured":"Fulton N, Mitsch S, Quesel J et al. (2015) KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: CADE, LNCS, vol 9195. Springer. https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"491_CR25","volume-title":"IJCAI\u201973","author":"C Hewitt","year":"1973","unstructured":"Hewitt C, Bishop P, Steiger R (1973) A universal modular ACTOR formalism for artificial intelligence. In: IJCAI\u201973. William Kaufmann. http:\/\/ijcai.org\/Proceedings\/73\/Papers\/027B.pdf"},{"key":"491_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"FMCO\u201910, LNCS","author":"EB Johnsen","year":"2010","unstructured":"Johnsen EB, H\u00e4hnle R, Sch\u00e4fer J et al. (2010) ABS: a core language for abstract behavioral specification. In: Aichernig BK, de Boer FS, Bonsangue MM (eds) FMCO\u201910, LNCS, vol 6957. Springer. https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"491_CR27","doi-asserted-by":"publisher","unstructured":"Kamburjan E, Din CC, H\u00e4hnle R et al. (2020) Behavioral contracts for cooperative scheduling. In: Ahrendt W, Beckert B, Bubel R etal (eds) Deductive verification: the state of the future, LNCS, vol 12345. Springer. https:\/\/doi.org\/10.1007\/978-3-030-64354-6_4","DOI":"10.1007\/978-3-030-64354-6_4"},{"issue":"3","key":"491_CR28","doi-asserted-by":"publisher","first-page":"10.1007\/s00165\u2013","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2015","unstructured":"Din CC, Owe O (2015) Compositional reasoning about active objects with shared futures. Formal Asp Comput 27(3):10.1007\/s00165\u2013014\u20130322\u2013y","journal-title":"Formal Asp Comput"},{"key":"491_CR29","doi-asserted-by":"publisher","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"491_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_22","volume-title":"TABLEAUX, LNCS","author":"E Kamburjan","year":"2019","unstructured":"Kamburjan E (2019) Behavioral program logic. In: Cerrito S, Popescu A (eds) TABLEAUX, LNCS, vol 11714. Springer. https:\/\/doi.org\/10.1007\/978-3-030-29026-9_22"},{"key":"491_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6_9","volume-title":"The KeY book, LNCS","author":"D Grahl","year":"2016","unstructured":"Grahl D, Bubel R, Mostowski W et al. (2016) Modular specification and verification. In: The KeY book, LNCS, vol 10001. Springer. https:\/\/doi.org\/10.1007\/978-3-319-49812-6_9"},{"key":"491_CR32","doi-asserted-by":"publisher","unstructured":"Jansen V (1995) Regulation of predator-prey systems through spatial interactions: a possible solution to the paradox of enrichment. Oikos 74. https:\/\/doi.org\/10.2307\/3545983","DOI":"10.2307\/3545983"},{"key":"491_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"CADE, LNCS","author":"CC Din","year":"2015","unstructured":"Din CC, Bubel R, H\u00e4hnle R (2015) KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty A, Middeldorp A (eds) CADE, LNCS, vol 9195. Springer. https:\/\/doi.org\/10.1007\/978-3-319-21401-6_35"},{"key":"491_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_19","volume-title":"ICFEM","author":"E Kamburjan","year":"2016","unstructured":"Kamburjan E, Din CC, Chen T (2016) Session-based compositional analysis for actor-based languages using futures. In: Ogata K, Lawford M, Liu S (eds) ICFEM. https:\/\/doi.org\/10.1007\/978-3-319-47846-3_19"},{"key":"491_CR35","doi-asserted-by":"publisher","unstructured":"Kamburjan E, Wasser N (2022) The right kind of non-determinism: using concurrency to verify C programs with underspecified semantics. In: Aubert C, Giusto CD, Safina L etal (eds) ICE. https:\/\/doi.org\/10.4204\/EPTCS.365.1","DOI":"10.4204\/EPTCS.365.1"},{"key":"491_CR36","doi-asserted-by":"publisher","unstructured":"Kamburjan E, Scaletta M, Rollshausen N (2023) Deductive verification of active objects with crowbar. Sci Comput Program 226. https:\/\/doi.org\/10.1016\/J.SCICO.2023.102928","DOI":"10.1016\/J.SCICO.2023.102928"},{"key":"491_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51060-1_12","volume-title":"Active object languages: current research trends, LNCS","author":"E Kamburjan","year":"2024","unstructured":"Kamburjan E, Lienhardt M (2024) Type-based verification of delegated control in hybrid systems. In: Active object languages: current research trends, LNCS, vol 14360. Springer. https:\/\/doi.org\/10.1007\/978-3-031-51060-1_12"},{"key":"491_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_1","volume-title":"ISoLA (1), LNCS","author":"D Gurov","year":"2020","unstructured":"Gurov D, H\u00e4hnle R, Kamburjan E (2020) Who carries the burden of modularity? - introduction to ISoLA 2020 track on modularity and (de-)composition in verification. In: ISoLA (1), LNCS, vol 12476. Springer. https:\/\/doi.org\/10.1007\/978-3-030-61362-4_1"},{"key":"491_CR39","doi-asserted-by":"publisher","unstructured":"Platzer A (2017) A complete uniform substitution calculus for differential dynamic logic. J Automated Reasoning 59(2). https:\/\/doi.org\/10.1007\/S10817-016-9385-1","DOI":"10.1007\/S10817-016-9385-1"},{"key":"491_CR40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_34","volume-title":"CAV, LNCS","author":"I Hasuo","year":"2012","unstructured":"Hasuo I, Suenaga K (2012) Exercises in nonstandard static analysis of hybrid systems. In: Madhusudan P, Seshia SA (eds) CAV, LNCS, vol 7358. Springer. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_34"},{"key":"491_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64276-1_14","volume-title":"ICTAC, LNCS","author":"S Goncharov","year":"2020","unstructured":"Goncharov S, Neves R, Proen\u00e7a J (2020) Implementing hybrid semantics: from functional to imperative. In: Pun VKI, Stolz V, Sim\u00e3o A (eds) ICTAC, LNCS, vol 12545. Springer. https:\/\/doi.org\/10.1007\/978-3-030-64276-1_14"},{"key":"491_CR42","doi-asserted-by":"publisher","unstructured":"Mendes P, Correia R, Neves R et al. (2024) Formal simulation and visualisation of hybrid programs. In FMAS@iFM. https:\/\/doi.org\/10.4204\/EPTCS.411.2","DOI":"10.4204\/EPTCS.411.2"},{"key":"491_CR43","doi-asserted-by":"publisher","unstructured":"Ghassemi F, Zhiany S, Abbasi N et al. (2025) Reachability analysis of hybrid rebeca models. J Syst Archit 167. https:\/\/doi.org\/10.1016\/J.SYSARC.2025.103493","DOI":"10.1016\/J.SYSARC.2025.103493"},{"key":"491_CR44","unstructured":"Zhiany S, Ghassemi F, Abbasimoghadam N et al. (2024) Hybrid rebeca revisited. CoRR Abs\/2411.03160. https:\/\/arxiv.org\/abs\/2411.03160 2411.03160"},{"key":"491_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-53733-7_8","volume-title":"LATA","author":"R Lanotte","year":"2017","unstructured":"Lanotte R, Merro M (2017) A calculus of cyber-physical systems. In: Drewes F, Mart\u00edn-Vide C, Truthe B (eds) LATA. https:\/\/doi.org\/10.1007\/978-3-319-53733-7_8"},{"key":"491_CR46","doi-asserted-by":"publisher","unstructured":"Hennessy M, Regan T (1995) A process algebra for timed systems. Inf Comput 117(2). https:\/\/doi.org\/10.1006\/INCO.1995.1041","DOI":"10.1006\/INCO.1995.1041"},{"key":"491_CR47","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A calculus of communicating systems, LNCS","author":"R Milner","year":"1980","unstructured":"Milner R (1980) A calculus of communicating systems, LNCS, vol 92. Springer. https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"key":"491_CR48","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36580-X_32","volume-title":"HSCC, LNCS","author":"WC Rounds","year":"2003","unstructured":"Rounds WC, Song H (2003) The phi-calculus: a language for distributed control of reconfigurable embedded systems. In: HSCC, LNCS, vol 2623. Springer. https:\/\/doi.org\/10.1007\/3-540-36580-X_32"},{"key":"491_CR49","unstructured":"Khadim U (2006) A comparative study of process algebras for hybrid systems. Computer science reports, technische universiteit eindhoven. https:\/\/research.tue.nl\/files\/2371657\/200623.pdf. accessed 17.01.2026"},{"key":"491_CR50","doi-asserted-by":"publisher","unstructured":"Cuijpers PJL, Reniers MA (2005) Hybrid process algebra. J Log Algebraic Methods Program 62(2). https:\/\/doi.org\/10.1016\/J.JLAP.2004.02.001","DOI":"10.1016\/J.JLAP.2004.02.001"},{"key":"491_CR51","doi-asserted-by":"publisher","unstructured":"Bos V, Kleijn JJT (2003) Redesign of a systems engineering language: formalisation of X. Formal Aspects Comput 15(4). https:\/\/doi.org\/10.1007\/S00165-003-0017-2","DOI":"10.1007\/S00165-003-0017-2"},{"key":"491_CR52","doi-asserted-by":"publisher","unstructured":"Bergstra JA, Klop JW (1985) Algebra of communicating processes with abstraction. Theor Comput Sci 37. https:\/\/doi.org\/10.1016\/0304-3975(85)90088-X","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"491_CR53","doi-asserted-by":"publisher","unstructured":"Bergstra JA, Middelburg CA (2005) Process algebra for hybrid systems. Theor Comput Sci 335(2\u20133). https:\/\/doi.org\/10.1016\/j.tcs.2004.04.019","DOI":"10.1016\/j.tcs.2004.04.019"},{"key":"491_CR54","doi-asserted-by":"publisher","unstructured":"Galpin V, Bortolussi L, Hillston J (2013) HYPE: hybrid modelling by composition of flows. Formal Aspects Comput 25(4). https:\/\/doi.org\/10.1007\/S00165-011-0189-0","DOI":"10.1007\/S00165-011-0189-0"},{"key":"491_CR55","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2017.16","volume-title":"ACSD","author":"S Lunel","year":"2017","unstructured":"Lunel S, Boyer B, Talpin J (2017) Compositional proofs in differential dynamic logic dL. In: ACSD. IEEE Computer Society. https:\/\/doi.org\/10.1109\/ACSD.2017.16"},{"key":"491_CR56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_22","volume-title":"FM, LNCS","author":"S Lunel","year":"2019","unstructured":"Lunel S, Mitsch S, Boyer B et al. (2019) Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In: Ter Beek MH, McIver A, Oliveira JN (eds) FM, LNCS, vol 11800. Springer. https:\/\/doi.org\/10.1007\/978-3-030-30942-8_22"},{"key":"491_CR57","doi-asserted-by":"publisher","unstructured":"M\u00fcller A, Mitsch S, Retschitzegger W et al. (2018) Tactical contract composition for hybrid system component verification. STTT 20(6). https:\/\/doi.org\/10.1007\/S10009-018-0502-9","DOI":"10.1007\/S10009-018-0502-9"},{"key":"491_CR58","doi-asserted-by":"publisher","unstructured":"Baar T, Staroletov S (2019) A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier. Modeling Anal Inf Syst 25(5). https:\/\/doi.org\/10.18255\/1818-1015-465-480","DOI":"10.18255\/1818-1015-465-480"},{"key":"491_CR59","doi-asserted-by":"publisher","unstructured":"Bourke T, Pouzet M (2013) Z\u00e8lus: a synchronous language with ODEs. In: Belta C, Ivancic F (eds) 16th International Conference on Hybrid Systems: Computation and Control (HSCC\u201913). https:\/\/doi.org\/10.1145\/2461328.2461348","DOI":"10.1145\/2461328.2461348"},{"key":"491_CR60","doi-asserted-by":"publisher","unstructured":"Benveniste A, Berry G (1991) The synchronous approach to reactive and real-time systems. Proc IEEE 79(9). https:\/\/doi.org\/10.1109\/5.97297","DOI":"10.1109\/5.97297"},{"key":"491_CR61","doi-asserted-by":"publisher","unstructured":"Benveniste A, Caillaud B, Nickovic D et al. (2018) Contracts for system design. Found Trends Electron Des Autom 12(2\u20133). https:\/\/doi.org\/10.1561\/1000000053","DOI":"10.1561\/1000000053"},{"key":"491_CR62","doi-asserted-by":"publisher","unstructured":"Alur R, Courcoubetis C, Halbwachs N et al. (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138(1). https:\/\/doi.org\/10.1016\/0304-3975(94)00202-T","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"491_CR63","doi-asserted-by":"publisher","unstructured":"Lynch NA, Segala R, Vaandrager FW (2003) Hybrid I\/O automata. Inf Comput 185(1). https:\/\/doi.org\/10.1016\/S0890-5401(03)00067-1","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"491_CR64","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2013.6669815","volume-title":"ECC 2013","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9 A, Frehse G (2013) Modular, hierarchical models of control systems in SpaceEx. In: ECC 2013. IEEE. https:\/\/doi.org\/10.23919\/ECC.2013.6669815"},{"key":"491_CR65","doi-asserted-by":"publisher","unstructured":"Frehse G, Han Z, Krogh B (2004) Assume-guarantee reasoning for hybrid i\/o-automata by over-approximation of continuous interaction. In CDC 2004. https:\/\/doi.org\/10.1109\/CDC.2004.1428676","DOI":"10.1109\/CDC.2004.1428676"},{"key":"491_CR66","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_24","volume-title":"HSCC, LNCS","author":"TA Henzinger","year":"2001","unstructured":"Henzinger TA, Minea M, Prabhu VS (2001) Assume-guarantee reasoning for hierarchical hybrid systems. In: Benedetto MDD, Sangiovanni-Vincentelli AL (eds) HSCC, LNCS, vol 2034. Springer. https:\/\/doi.org\/10.1007\/3-540-45351-2_24"},{"key":"491_CR67","doi-asserted-by":"publisher","first-page":"171","DOI":"10.5555\/197600.197614","volume-title":"From CSP to hybrid systems","author":"H Jifeng","year":"1994","unstructured":"Jifeng H (1994) From CSP to hybrid systems. Prentice Hall International (UK) Ltd, pp 171\u2013189. https:\/\/doi.org\/10.5555\/197600.197614"},{"key":"491_CR68","doi-asserted-by":"publisher","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"491_CR69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_4","volume-title":"ISoLA (I), LNCS","author":"B Beckert","year":"2020","unstructured":"Beckert B, Kirsten M, Klamroth J et al. (2020) Modular verification of JML contracts using bounded model checking. In: Margaria T, Steffen B (eds) ISoLA (I), LNCS, vol 12476. Springer. https:\/\/doi.org\/10.1007\/978-3-030-61362-4_4"},{"key":"491_CR70","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/978-3-319-10575-8_20","volume-title":"Combining model checking and deduction","author":"N Shankar","year":"2018","unstructured":"Shankar N (2018) Combining model checking and deduction. Springer International Publishing, Cham, pp 651\u2013684. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_20"},{"key":"491_CR71","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_14","volume-title":"NFM","author":"A Sogokon","year":"2017","unstructured":"Sogokon A, Jackson PB, Johnson TT (2017) Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants. In: Barrett CW, Davies M, Kahsai T (eds) NFM. https:\/\/doi.org\/10.1007\/978-3-319-57288-8_14"},{"key":"491_CR72","unstructured":"Teuber S, Ulbrich M, Platzer A et al. (2025) Heterogeneous dynamic logic: provability modulo program theories. CoRR Abs\/2507.08581. https:\/\/arxiv.org\/abs\/2507.08581 2507.08581"},{"key":"491_CR73","doi-asserted-by":"publisher","unstructured":"de Boer Fs, de Gouw S (2022) Reasoning about active objects: a sound and complete assertional proof method. In: The logic of software. A tasting menu of formal methods, LNCS, vol 13360. Springer. https:\/\/doi.org\/10.1007\/978-3-031-08166-8_9","DOI":"10.1007\/978-3-031-08166-8_9"},{"key":"491_CR74","doi-asserted-by":"publisher","unstructured":"Din CC, H\u00e4hnle R, Henrio L et al. (2024) Locally abstract, globally concrete semantics of concurrent programming languages. ACM Trans Program Lang Syst 46(1). https:\/\/doi.org\/10.1145\/3648439","DOI":"10.1145\/3648439"},{"key":"491_CR75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08166-8_23","volume-title":"The logic of software. A tasting menu of formal methods, LNCS","author":"SLT Tarifa","year":"2022","unstructured":"Tarifa SLT, Beckert B, Bubel R et al. (2022) Locally abstract globally concrete semantics of time and resource aware active objects. In: Ahrendt W (ed) The logic of software. A tasting menu of formal methods, LNCS, vol 13360. Springer. https:\/\/doi.org\/10.1007\/978-3-031-08166-8_23"},{"key":"491_CR76","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rk J, de Boer FS, Johnsen EB et al. (2013) User-defined schedulers for real-time concurrent objects. Innov Syst Softw Eng 9(1). https:\/\/doi.org\/10.1007\/S11334-012-0184-5","DOI":"10.1007\/S11334-012-0184-5"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00491-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-026-00491-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00491-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T09:11:58Z","timestamp":1772788318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-026-00491-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2]]},"references-count":76,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["491"],"URL":"https:\/\/doi.org\/10.1007\/s10703-026-00491-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2]]},"assertion":[{"value":"20 September 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 February 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2026","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":"3"}}