{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T04:04:28Z","timestamp":1750910668798,"version":"3.41.0"},"publisher-location":"Cham","reference-count":183,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031676949"},{"type":"electronic","value":"9783031676956"}],"license":[{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-67695-6_1","type":"book-chapter","created":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T14:03:04Z","timestamp":1730383384000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The ARCH-COMP Friendly Verification Competition for\u00a0Continuous and\u00a0Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]},{"given":"Lei","family":"Bu","sequence":"additional","affiliation":[]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[]},{"given":"Goran","family":"Frehse","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Geretti","sequence":"additional","affiliation":[]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schupp","sequence":"additional","affiliation":[]},{"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: Arch-comp21 category report: stochastic models. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2021). EPiC Series in Computing, vol.\u00a080, pp. 55\u201389. EasyChair (2021). https:\/\/doi.org\/10.29007\/dprv","DOI":"10.29007\/dprv"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: ARCH-COMP19 category report: stochastic modelling. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2019). EPiC Series in Computing, vol.\u00a061, pp. 62\u2013102. EasyChair (2019). https:\/\/doi.org\/10.29007\/f2vb","DOI":"10.29007\/f2vb"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: Arch-comp20 category report: stochastic models. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2020). EPiC Series in Computing, vol.\u00a074, pp. 76\u2013106. EasyChair (2020). https:\/\/doi.org\/10.29007\/mqzc","DOI":"10.29007\/mqzc"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: ARCH-COMP18 category report: stochastic modelling. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2018). EPiC Series in Computing, vol.\u00a054, pp. 71\u2013103. EasyChair (2018). https:\/\/doi.org\/10.29007\/7ks7","DOI":"10.29007\/7ks7"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: ARCH-COMP22 Category Report: Stochastic Models, vol.\u00a090, pp. 113\u2013141. EasyChair (2022). https:\/\/doi.org\/10.29007\/LSVC","DOI":"10.29007\/LSVC"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-40196-1_22","volume-title":"Quantitative Evaluation of Systems","author":"D Adzkiya","year":"2013","unstructured":"Adzkiya, D., Abate, A.: VeriSiMPL: verification via biSimulations of MPL models. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 274\u2013277. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_22"},{"issue":"1","key":"1_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10626-015-0218-x","volume":"26","author":"D Adzkiya","year":"2016","unstructured":"Adzkiya, D., Zhang, Y., Abate, A.: VeriSiMPL 2: an open-source software for the verification of max-plus-linear systems. Discrete Event Dyn. Syst. 26(1), 109\u2013145 (2016). https:\/\/doi.org\/10.1007\/s10626-015-0218-x","journal-title":"Discrete Event Dyn. Syst."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Akintunde, M.E., Botoeva, E., Kouvaros, P., Lomuscio, A.: Formal verification of neural agents in non-deterministic environments. In: International Conference on Autonomous Agents and Multiagent Systems, AAMAS, pp. 25\u201333 (2020)","DOI":"10.1007\/s10458-021-09529-3"},{"key":"1_CR9","unstructured":"ARCH-COMP repository of benchmark models, documentation, and repeatability packages. https:\/\/gitlab.com\/goranf\/ARCH-COMP"},{"key":"1_CR10","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015)"},{"issue":"2","key":"1_CR11","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1109\/TAC.2019.2906432","volume":"65","author":"M Althoff","year":"2020","unstructured":"Althoff, M.: Reachability analysis of large linear systems with uncertain inputs in the Krylov subspace. IEEE Trans. Autom. Control 65(2), 477\u2013492 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Althoff, M., et al.: ARCH-COMP20 category report: continuous and hybrid systems with linear continuous dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a074, pp. 16\u201348 (2020)","DOI":"10.29007\/7dt2"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Althoff, M., et al.: ARCH-COMP17 category report: continuous and hybrid systems with linear continuous dynamics. In: International Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 143\u2013159 (2017)","DOI":"10.29007\/4dcn"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Althoff, M., et al.: ARCH-COMP18 category report: continuous and hybrid systems with linear continuous dynamics. In: International Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 23\u201352 (2018)","DOI":"10.29007\/73mb"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Althoff, M., et al.: ARCH-COMP19 category report: continuous and hybrid systems with linear continuous dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a061, pp. 14\u201340 (2019)","DOI":"10.29007\/bj1w"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Hybrid Systems: Computation and Control, pp. 45\u201354 (2012)","DOI":"10.1145\/2185632.2185643"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Althoff, M., et al.: ARCH-COMP21 category report: continuous and hybrid systems with linear continuous dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems, vol.\u00a080, pp. 1\u201331 (2021). https:\/\/doi.org\/10.29007\/lhbw. https:\/\/easychair.org\/publications\/paper\/81BS","DOI":"10.29007\/lhbw"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Althoff, M., Forets, M., Schilling, C., Wetzlinger, M.: ARCH-COMP22 category report: continuous and hybrid systems with linear continuous dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a090, pp. 58\u201385. EasyChair (2022). https:\/\/doi.org\/10.29007\/mmzc. https:\/\/easychair.org\/publications\/paper\/b6cN","DOI":"10.29007\/mmzc"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Althoff, M.: Time-triggered conversion of guards for reachability analysis of hybrid automata. In: International Conference on Formal Modelling and Analysis of Timed Systems, pp. 133\u2013150 (2017)","DOI":"10.1007\/978-3-319-65765-3_8"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: HyLAA: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 173\u2013178 (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Bak, S., Tran, H.D., Johnson, T.T.: Numerical verification of affine systems with up to a billion dimensions. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 23\u201332 (2019)","DOI":"10.1145\/3302504.3311792"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-319-96145-3_13","volume-title":"Computer Aided Verification","author":"A Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: A direct encoding for NNC Polyhedra. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 230\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_13"},{"issue":"2","key":"1_CR26","doi-asserted-by":"publisher","first-page":"7979","DOI":"10.3182\/20080706-5-KR-1001.01348","volume":"41","author":"DA van Beek","year":"2008","unstructured":"van Beek, D.A., Reniers, M.A., Rooda, J.E., Schiffelers, R.R.: Concrete syntax and semantics of the compositional interchange format for hybrid systems. IFAC Proc. Vol. 41(2), 7979\u20137986 (2008)","journal-title":"IFAC Proc. Vol."},{"issue":"5","key":"1_CR27","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1109\/TAC.2004.828315","volume":"49","author":"A Bemporad","year":"2004","unstructured":"Bemporad, A.: Efficient conversion of mixed logical dynamical systems into an equivalent piecewise affine form. IEEE Trans. Autom. Control 49(5), 832\u2013838 (2004)","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11558958_8","volume-title":"Applied Parallel Computing. State of the Art in Scientific Computing","author":"M Berz","year":"2006","unstructured":"Berz, M., Makino, K.: Performance of Taylor model methods for validated integration of ODEs. In: Dongarra, J., Madsen, K., Wa\u015bniewski, J. (eds.) PARA 2004. LNCS, vol. 3732, pp. 65\u201373. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11558958_8"},{"key":"1_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-031-30820-8_29","volume-title":"TACAS 2023","author":"D Beyer","year":"2023","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) 13994. LNCS, vol. 13994, pp. 495\u2013522. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29"},{"issue":"16","key":"1_CR30","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.ifacol.2018.08.014","volume":"51","author":"HA Blom","year":"2018","unstructured":"Blom, H.A., Ma, H., Bakker, G.B.: Interacting particle system-based estimation of reach probability for a generalized stochastic hybrid system. IFAC-PapersOnLine 51(16), 79\u201384 (2018)","journal-title":"IFAC-PapersOnLine"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39\u201344 (2019). https:\/\/doi.org\/10.1145\/3302504.3311804","DOI":"10.1145\/3302504.3311804"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Viry, F., Podelski, A., Schilling, C.: Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control, pp. 41\u201350 (2018)","DOI":"10.1145\/3178126.3178128"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-54577-5_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bogomolov","year":"2017","unstructured":"Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 589\u2013606. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_34"},{"key":"1_CR34","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 (2017)","DOI":"10.1145\/3018610.3018616"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Bohrer, R., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: Veriphy: verified controller executables from verified cyber-physical system models. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617\u2013630 (2018). https:\/\/doi.org\/10.1145\/3192366.3192406","DOI":"10.1145\/3192366.3192406"},{"key":"1_CR36","unstructured":"Bouissou, M., Houdebine, J.: Inconsistency detection in KB3 models. In: ESREL 2002 (2002)"},{"key":"1_CR37","unstructured":"Bouissou, M., Houdebine, S., Houdebine, J.C.: Reference manual of the Figaro probabilistic modelling language (2019)"},{"key":"1_CR38","unstructured":"Bouissou, M., Khan, S.: Bridging the dependability and model checking worlds. In: Congr\u00e8s Lambda Mu 23 \u00abInnovations et ma\u00eetrise des risques pour un avenir durable\u00bb-23e Congr\u00e8s de Ma\u00eetrise des Risques et de S\u00fbret\u00e9 de Fonctionnement, Institut pour la Ma\u00eetrise des Risques (2022)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Bourke, T., Pouzet, M.: Z\u00e9lus: a synchronous language with ODEs. In: International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 113\u2013118 (2013)","DOI":"10.1145\/2461328.2461348"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Bresolin, D., Collins, P., Geretti, L., Segala, R., Villa, T., Gonzalez, S.V.: A computable and compositional semantics for hybrid automata. In: International Conference on Hybrid Systems: Computation and Control HSCC. ACM (2020)","DOI":"10.1145\/3365365.3382202"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Bu, L., et al.: ARCH-COMP20 category report: hybrid systems with piecewise constant dynamics and bounded model checking. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 1\u201315. EasyChair (2020)","DOI":"10.29007\/bhwx"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Bu, L., Frehse, G., Kundu, A., Ray, R., Shi, Y., Zaffanella, E.: ARCH-COMP22 category report: hybrid systems with piecewise constant dynamics and bounded model checking. In: International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a090, pp. 44\u201357. EasyChair (2022)","DOI":"10.29007\/lnzf"},{"key":"1_CR43","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: Design, Automation and Test in Europe (DATE), pp. 1512\u20131517 (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Li, X.: BACH: bounded reachability checker for linear hybrid automata. In: Formal Methods in Computer-Aided Design (FMCAD), pp.\u00a01\u20134 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Bu, L., Ray, R., Schupp, S.: ARCH-COMP17 category report: bounded model checking of hybrid systems with piecewise constant dynamics. In: ARCH 2017. International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek). EPiC Series in Computing, vol.\u00a048, pp. 134\u2013142. EasyChair (2017)","DOI":"10.29007\/rvk6"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Bu, L., Ray, R., Schupp, S.: ARCH-COMP18 category report: bounded model checking of hybrid systems with piecewise constant dynamics. In: ARCH 2018. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a054, pp. 14\u201322. EasyChair (2018)","DOI":"10.29007\/q5tq"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Bu, L., Ray, R., Schupp, S.: ARCH-COMP19 category report: bounded model checking of hybrid systems with piecewise constant dynamics. In: ARCH 2019. International Workshop on Applied Verification of Continuous and Hybrid Systems, part of CPS-IoT Week. EPiC Series in Computing, vol.\u00a061, pp. 120\u2013128. EasyChair (2019)","DOI":"10.29007\/g965"},{"issue":"6","key":"1_CR48","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1007\/s10009-020-00563-2","volume":"22","author":"CE Budde","year":"2020","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transfer 22(6), 759\u2013780 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In: Static Analysis, pp. 312\u2013331 (2015)","DOI":"10.1007\/978-3-662-48288-9_18"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Cauchi, N., Abate, A.: StocHy: automated verification and synthesis of stochastic processes. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2019)","DOI":"10.1007\/978-3-030-17465-1_14"},{"key":"1_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"1_CR52","doi-asserted-by":"publisher","unstructured":"Chen, X., Althoff, M., Immler, F.: Arch-comp17 category report: continuous systems with nonlinear dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a048, pp. 160\u2013169. EasyChair (2017). https:\/\/doi.org\/10.29007\/v6g4","DOI":"10.29007\/v6g4"},{"key":"1_CR53","unstructured":"Chraibi, H., Houbedine, J., Sibler, A.: PyCATSHOO: toward a new platform dedicated to dynamic reliability assessments of hybrid systems. In: 13th International Conference on Probabilistic Safety Assessment and Management (PSAM 13), Seoul, Korea (2016)"},{"key":"1_CR54","unstructured":"Chraibi, H., Houbedine, J., Sibler, A.: Pycatshoo: toward a new platform dedicated to dynamic reliability assessments of hybrid systems. In: PSAM Congress (2016)"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: TACAS, pp. 52\u201367 (2015)","DOI":"10.1007\/978-3-662-46681-0_4"},{"key":"1_CR56","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1613\/jair.1.12716","volume":"72","author":"A Corso","year":"2021","unstructured":"Corso, A., Moss, R.J., Koren, M., Lee, R., Kochenderfer, M.J.: A survey of algorithms for black-box safety validation of cyber-physical systems. J. Artif. Intell. Res. 72, 377\u2013428 (2021). https:\/\/doi.org\/10.1613\/jair.1.12716","journal-title":"J. Artif. Intell. Res."},{"key":"1_CR57","unstructured":"Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliable Comput. 17 (2012)"},{"key":"1_CR58","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-35257-7_10","volume-title":"Theoretical Aspects of Software Engineering (TASE)","author":"J Delicaris","year":"2023","unstructured":"Delicaris, J., Schupp, S., \u00c1br\u00e1ham, E., Remke, A.: Maximizing reachability probabilities in rectangular automata with random clocks. In: David, C., Sun, M. (eds.) TASE 2023. LNCS, vol. 13931. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35257-7_10"},{"key":"1_CR59","doi-asserted-by":"publisher","unstructured":"Dokhanchi, A., Yaghoubi, S., Hoxha, B., Fainekos, G.: ARCH-COMP17 category report: preliminary results on the falsification benchmarks. In: ARCH 2017. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, pp. 170\u2013174. EasyChair (2017). https:\/\/doi.org\/10.29007\/wmf5","DOI":"10.29007\/wmf5"},{"key":"1_CR60","doi-asserted-by":"publisher","unstructured":"Dokhanchi, A., et al.: ARCH-COMP18 category report: results on the falsification benchmarks. In: ARCH 2018. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, pp. 104\u2013109. EasyChair (2018). https:\/\/doi.org\/10.29007\/t85q","DOI":"10.29007\/t85q"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of Computer-Aided Verification, pp. 167\u2013170 (2010)","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 68\u201382 (2015)","DOI":"10.1007\/978-3-662-46681-0_5"},{"key":"1_CR63","doi-asserted-by":"publisher","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: ACM International Conference on Hybrid Systems: Computation and Control, HSCC, pp. 157\u2013168 (2019). https:\/\/doi.org\/10.1145\/3302504.3311807","DOI":"10.1145\/3302504.3311807"},{"key":"1_CR64","doi-asserted-by":"publisher","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine 51(16), 151\u2013156 (2018). https:\/\/doi.org\/10.1016\/j.ifacol.2018.08.026. iFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018","DOI":"10.1016\/j.ifacol.2018.08.026"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"NASA Formal Methods","author":"S Dutta","year":"2018","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 121\u2013138. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_9"},{"key":"1_CR66","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2021 category report: falsification with validation of results. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2021). EPiC Series in Computing, pp. 133\u2013152. EasyChair (2021). https:\/\/doi.org\/10.29007\/xwl1","DOI":"10.29007\/xwl1"},{"key":"1_CR67","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2020 category report: falsification. In: ARCH 2020. International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2020). EPiC Series in Computing, pp. 140\u2013152. EasyChair (2020). https:\/\/doi.org\/10.29007\/trr1","DOI":"10.29007\/trr1"},{"key":"1_CR68","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2019 category report: falsification. In: ARCH 2019. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, pp. 129\u2013140. EasyChair (2019). https:\/\/doi.org\/10.29007\/68dk","DOI":"10.29007\/68dk"},{"key":"1_CR69","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: Arch-comp 2022 category report: falsification with ubounded resources. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2022). EPiC Series in Computing, pp. 204\u2013221. EasyChair (2022). https:\/\/doi.org\/10.29007\/fhnk","DOI":"10.29007\/fhnk"},{"issue":"3","key":"1_CR70","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3459605","volume":"31","author":"G Ernst","year":"2021","unstructured":"Ernst, G., Sedwards, S., Zhang, Z., Hasuo, I.: Falsification of hybrid systems using adaptive probabilistic search. ACM Trans. Model. Comput. Simul. (TOMACS) 31(3), 1\u201322 (2021)","journal-title":"ACM Trans. Model. Comput. Simul. (TOMACS)"},{"key":"1_CR71","unstructured":"Everdij, M., Blom, H.: Hybrid state Petri nets which have the analysis power of stochastic hybrid systems and the formal verification power of automata. In: Pawlewski, P. (ed.) Petri Nets, chap.\u00a012, pp. 227\u2013252. I-Tech Education and Publishing, Vienna (2010)"},{"key":"1_CR72","unstructured":"Immler, F., Althoff, M., et al.: Symreach. https:\/\/github.com\/mahendrasinghtomar\/SymReach"},{"key":"1_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11940197_12","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"GE Fainekos","year":"2006","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) FATES\/RV -2006. LNCS, vol. 4262, pp. 178\u2013192. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11940197_12"},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Computer Aided Verification, pp. 531\u2013538 (2016)","DOI":"10.1007\/978-3-319-41528-4_29"},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Fan, J., Huang, C., Li, W., Chen, X., Zhu, Q.: Reachnn*: a tool for reachability analysis of neural-network controlled systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA) (2020)","DOI":"10.1007\/978-3-030-59152-6_30"},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Fijalkow, N., Ouaknine, J., Pouly, A., Sousa-Pinto, J., Worrell, J.: On the decidability of reachability in linear time-invariant systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 77\u201386 (2019)","DOI":"10.1145\/3302504.3311796"},{"key":"1_CR77","doi-asserted-by":"publisher","unstructured":"Formica, F., Fan, T., Rajhans, A., Pantelic, V., Lawford, M., Menghi, C.: Simulation-based testing of simulink models with test sequence and test assessment blocks. IEEE Trans. Softw. Eng. 1\u201319 (2023). https:\/\/doi.org\/10.1109\/TSE.2023.3343753","DOI":"10.1109\/TSE.2023.3343753"},{"key":"1_CR78","doi-asserted-by":"publisher","DOI":"10.1145\/3624745","author":"F Formica","year":"2023","unstructured":"Formica, F., Tony, F., Menghi, C.: Search-based software testing driven by automatically generated and manually defined fitness functions. ACM Trans. Softw. Eng. Methodol. (2023). https:\/\/doi.org\/10.1145\/3624745","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR79","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":"1_CR80","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: International Conference on Hybrid Systems: Computation and Control, HSCC 2011, pp. 43\u201352. ACM (2011). https:\/\/doi.org\/10.1145\/1967701.1967710","DOI":"10.1145\/1967701.1967710"},{"key":"1_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11560647_17","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"M Fr\u00e4nzle","year":"2005","unstructured":"Fr\u00e4nzle, M., Hansen, M.R.: A robust interpretation of duration calculus. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 257\u2013271. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560647_17"},{"key":"1_CR82","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transfer 10, 263\u2013279 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"1_CR84","unstructured":"Frehse, G., et al.: ARCH-COMP19 category report: hybrid systems with piecewise constant dynamics. In: ARCH 2019. International Workshop on Applied Verification of Continuous and Hybrid Systems, part of CPS-IoT Week. EPiC Series in Computing, vol.\u00a061, pp. 1\u201313. EasyChair (2019)"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Frehse, G., Abate, A., Adzkiya, D., Bu, L., Giacobbe, M.: ARCH-COMP17 category report: hybrid systems with piecewise constant dynamics. In: ARCH 2017. International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek). EPiC Series in Computing, vol.\u00a048, pp. 124\u2013133. EasyChair (2017)","DOI":"10.29007\/n3km"},{"key":"1_CR86","doi-asserted-by":"crossref","unstructured":"Frehse, G., et al.: ARCH-COMP18 category report: hybrid systems with piecewise constant dynamics. In: ARCH 2018. International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH@ADHS. EPiC Series in Computing, vol.\u00a054, pp. 1\u201313. EasyChair (2018)","DOI":"10.29007\/p11g"},{"key":"1_CR87","unstructured":"Frehse, G.F.: Compositional verification of hybrid systems using simulation relations. Ph.D. thesis, Radboud University (2005)"},{"key":"1_CR88","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":"1_CR89","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\u00a0X: 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":"1_CR90","doi-asserted-by":"crossref","unstructured":"Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: Conference on Artificial Intelligence, (AAAI), pp. 6485\u20136492 (2018)","DOI":"10.1609\/aaai.v32i1.12107"},{"key":"1_CR91","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/978-3-031-10769-6_42","volume-title":"Automated Reasoning IJCAR","author":"J Gallicchio","year":"2022","unstructured":"Gallicchio, J., Tan, Y.K., Mitsch, S., Platzer, A.: Implicit definitions with differential equations for KeYmaera X - (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 723\u2013733. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_42"},{"key":"1_CR92","doi-asserted-by":"publisher","unstructured":"Garcia, L., Mitsch, S., Platzer, A.: Hyplc: hybrid programmable logic controller program translation for verification. In: ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS, pp. 47\u201356 (2019). https:\/\/doi.org\/10.1145\/3302509.3311036","DOI":"10.1145\/3302509.3311036"},{"key":"1_CR93","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-031-17196-3_22","volume-title":"RV 2022","author":"L Geretti","year":"2022","unstructured":"Geretti, L., Collins, P., Bresolin, D., Villa, T.: Automating numerical parameters along the evolution of a nonlinear system. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 336\u2013345. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_22"},{"key":"1_CR94","doi-asserted-by":"publisher","unstructured":"Geretti, L., et al.: Arch-comp20 category report: continuous and hybrid systems with nonlinear dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 49\u201375. EasyChair (2020). https:\/\/doi.org\/10.29007\/zkf6. https:\/\/easychair.org\/publications\/paper\/nrdD","DOI":"10.29007\/zkf6"},{"key":"1_CR95","doi-asserted-by":"publisher","unstructured":"Geretti, L., et al.: ARCH-COMP21 category report: continuous and hybrid systems with nonlinear dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21). EPiC Series in Computing, vol.\u00a080, pp. 32\u201354. EasyChair (2021). https:\/\/doi.org\/10.29007\/2jw8. https:\/\/easychair.org\/publications\/paper\/GWwz","DOI":"10.29007\/2jw8"},{"key":"1_CR96","doi-asserted-by":"publisher","unstructured":"Geretti, L., et al.: ARCH-COMP22 category report: continuous and hybrid systems with nonlinear dynamics. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22). EPiC Series in Computing, vol.\u00a090, pp. 86\u2013112. EasyChair (2022). https:\/\/doi.org\/10.29007\/fnzc. https:\/\/easychair.org\/publications\/paper\/JrQ4","DOI":"10.29007\/fnzc"},{"key":"1_CR97","doi-asserted-by":"publisher","unstructured":"Geretti, L., et al.: Arch-comp23 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23). EPiC Series in Computing, vol.\u00a096, pp. 61\u201388. EasyChair (2023). https:\/\/doi.org\/10.29007\/93f2. https:\/\/easychair.org\/publications\/paper\/T7LG","DOI":"10.29007\/93f2"},{"key":"1_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-78929-1_16","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2008","unstructured":"Girard, A., Le Guernic, C.: Zonotope\/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215\u2013228. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_16"},{"key":"1_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11730637_21","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2006","unstructured":"Girard, A., Le Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257\u2013271. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_21"},{"key":"1_CR100","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-69483-2_7","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"DP Guelev","year":"2017","unstructured":"Guelev, D.P., Wang, S., Zhan, N.: Compositional hoare-style reasoning about hybrid CSP in the duration calculus. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 110\u2013127. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_7"},{"issue":"6","key":"1_CR101","doi-asserted-by":"publisher","first-page":"2496","DOI":"10.1109\/TAC.2020.3010490","volume":"66","author":"S Haesaert","year":"2020","unstructured":"Haesaert, S., Soudjani, S.: Robust dynamic programming for temporal logic control of stochastic systems. IEEE Trans. Autom. Control 66(6), 2496\u20132511 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"1_CR102","doi-asserted-by":"publisher","first-page":"2333","DOI":"10.1137\/16M1079397","volume":"55","author":"S Haesaert","year":"2017","unstructured":"Haesaert, S., Zadeh Soudjani, S.E., Abate, A.: Verification of general Markov decision processes by approximate similarity relations and policy refinement. SIAM J. Control. Optim. 55(4), 2333\u20132367 (2017)","journal-title":"SIAM J. Control. Optim."},{"key":"1_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"1_CR104","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"T Henzinger","year":"2000","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Inan, K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"1_CR105","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: a polynomial arithmetic framework for verifying neural-network controlled systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA) (2022)","DOI":"10.1007\/978-3-031-19992-9_27"},{"issue":"5s","key":"1_CR106","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: reachability analysis of neural-network controlled systems. ACM Trans. Embed. Comput. Syst. (TECS) 18(5s), 1\u201322 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"1_CR107","doi-asserted-by":"crossref","unstructured":"Huerta y Munive, J.J., Struth, G.: Predicate transformer semantics for hybrid systems. JAR 66(1), 93\u2013139 (2022)","DOI":"10.1007\/s10817-021-09607-x"},{"key":"1_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-030-55754-6_22","volume-title":"NASA Formal Methods","author":"J H\u00fcls","year":"2020","unstructured":"H\u00fcls, J., Niehaus, H., Remke, A.: hpnmg: a C++ tool for model checking hybrid petri nets with general transitions. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 369\u2013378. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_22"},{"key":"1_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-662-46681-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Immler","year":"2015","unstructured":"Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 37\u201351. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_3"},{"key":"1_CR110","doi-asserted-by":"publisher","unstructured":"Immler, F., et al.: ARCH-COMP19 category report: continuous and hybrid systems with nonlinear dynamics. In: ARCH 2019. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a061, pp. 41\u201361. EasyChair (2019). https:\/\/doi.org\/10.29007\/m75b. https:\/\/easychair.org\/publications\/paper\/4FSh","DOI":"10.29007\/m75b"},{"key":"1_CR111","doi-asserted-by":"publisher","unstructured":"Immler, F., et al.: ARCH-COMP18 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse, G. (ed.) ARCH 2018. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a054, pp. 53\u201370. EasyChair (2018).https:\/\/doi.org\/10.29007\/mskf. https:\/\/easychair.org\/publications\/paper\/gjfh","DOI":"10.29007\/mskf"},{"key":"1_CR112","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig 2.0: verification of neural network controllers using taylor model preconditioning. In: International Conference on Computer-Aided Verification (2021)","DOI":"10.1007\/978-3-030-81685-8_11"},{"key":"1_CR113","doi-asserted-by":"publisher","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: International Conference on Hybrid Systems: Computation and Control, HSCC, pp. 169\u2013178. ACM (2019). https:\/\/doi.org\/10.1145\/3302504.3311806","DOI":"10.1145\/3302504.3311806"},{"key":"1_CR114","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-030-01090-4_11","volume-title":"Automated Technology for Verification and Analysis","author":"P Jagtap","year":"2018","unstructured":"Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic systems using barrier certificates. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 177\u2013193. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_11"},{"key":"1_CR115","doi-asserted-by":"crossref","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: International Conference on Hybrid Systems: Computation and Control, pp. 253\u2013262. ACM (2014)","DOI":"10.1145\/2562059.2562140"},{"key":"1_CR116","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: Arch-comp17 repeatability evaluation report. In: ARCH 2017. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a048, pp. 175\u2013180. EasyChair (2017). https:\/\/doi.org\/10.29007\/7hvk. https:\/\/easychair.org\/publications\/paper\/nMvb","DOI":"10.29007\/7hvk"},{"key":"1_CR117","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: Arch-comp18 repeatability evaluation report. In: ARCH 2018. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a054, pp. 128\u2013134. EasyChair (2018). https:\/\/doi.org\/10.29007\/n9t3. https:\/\/easychair.org\/publications\/paper\/9J6v","DOI":"10.29007\/n9t3"},{"key":"1_CR118","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: Arch-comp19 repeatability evaluation report. In: ARCH 2019. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a061, pp. 162\u2013169. EasyChair (2019).https:\/\/doi.org\/10.29007\/wbl3. https:\/\/easychair.org\/publications\/paper\/xvBM","DOI":"10.29007\/wbl3"},{"key":"1_CR119","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: Arch-comp20 repeatability evaluation report. In: ARCH 2020. International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 175\u2013183. EasyChair (2020). https:\/\/doi.org\/10.29007\/8dp4. https:\/\/easychair.org\/publications\/paper\/3W11","DOI":"10.29007\/8dp4"},{"key":"1_CR120","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: ARCH-COMP 2021 repeatability evaluation report. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21). EPiC Series in Computing, vol.\u00a080, pp. 153\u2013160. EasyChair (2021). https:\/\/doi.org\/10.29007\/zqdx. https:\/\/easychair.org\/publications\/paper\/cfpN","DOI":"10.29007\/zqdx"},{"key":"1_CR121","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: Arch-comp22 repeatability evaluation report. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2022). EPiC Series in Computing, vol.\u00a090, pp. 222\u2013230. EasyChair (2022). https:\/\/doi.org\/10.29007\/djqx. https:\/\/easychair.org\/publications\/paper\/LnDH","DOI":"10.29007\/djqx"},{"key":"1_CR122","doi-asserted-by":"publisher","unstructured":"Johnson, T.T.: Arch-comp23 repeatability evaluation report. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2023). EPiC Series in Computing, vol.\u00a096, pp. 189\u2013195. EasyChair (2023). https:\/\/doi.org\/10.29007\/q313. https:\/\/easychair.org\/publications\/paper\/TdVx","DOI":"10.29007\/q313"},{"key":"1_CR123","doi-asserted-by":"publisher","unstructured":"Johnson, T.T., et al.: Arch-comp21 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2021). EPiC Series in Computing, vol.\u00a080, pp. 90\u2013119. EasyChair (2021). https:\/\/doi.org\/10.29007\/kfk9","DOI":"10.29007\/kfk9"},{"key":"1_CR124","doi-asserted-by":"publisher","unstructured":"Johnson, T.T., et al.: Arch-comp20 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: ARCH 2020. International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2020). EPiC Series in Computing, vol.\u00a074, pp. 107\u2013139. EasyChair (2020). https:\/\/doi.org\/10.29007\/9xgv","DOI":"10.29007\/9xgv"},{"key":"1_CR125","doi-asserted-by":"publisher","first-page":"184","DOI":"10.29007\/rs5n","volume":"74","author":"E Kim","year":"2020","unstructured":"Kim, E., Duggirala, P.S.: Kaa: a python implementation of reachable set computation using bernstein polynomials. EPiC Ser. Comput. 74, 184\u2013196 (2020)","journal-title":"EPiC Ser. Comput."},{"key":"1_CR126","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-031-33170-1_2","volume-title":"NASA Formal Methods","author":"N Kochdumper","year":"2023","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: Rozier, K.Y., Chaudhuri, S. (eds.) NFM 2023. LNCS, vol. 13903, pp. 16\u201336. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2"},{"issue":"4","key":"1_CR127","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"1_CR128","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. Symb. Comput. 32, 231\u2013253 (2001)","journal-title":"Symb. Comput."},{"key":"1_CR129","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-53291-8_24","volume-title":"Computer Aided Verification","author":"A Lavaei","year":"2020","unstructured":"Lavaei, A., Khaled, M., Soudjani, S., Zamani, M.: AMYTISS: parallelized automated controller synthesis for large-scale stochastic systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 461\u2013474. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_24"},{"key":"1_CR130","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110617","volume":"146","author":"A Lavaei","year":"2022","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: a survey. Automatica 146, 110617 (2022)","journal-title":"Automatica"},{"issue":"6","key":"1_CR131","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1177\/0278364919846340","volume":"38","author":"K Leahy","year":"2019","unstructured":"Leahy, K., et al.: Control in belief space with temporal logic specifications using vision-based localization. Int. J. Robot. Res. 38(6), 702\u2013722 (2019)","journal-title":"Int. J. Robot. Res."},{"key":"1_CR132","doi-asserted-by":"crossref","unstructured":"Li, Y., Zhu, H., Braught, K., Shen, K., Mitra, S.: Verse: a python library for reasoning about multi-agent hybrid system scenarios. In: Computer Aided Verification, pp. 351\u2013364 (2023)","DOI":"10.1007\/978-3-031-37706-8_18"},{"key":"1_CR133","doi-asserted-by":"publisher","unstructured":"Loos, S.M., Platzer, A.: Differential refinement logic. In: Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS, pp. 505\u2013514 (2016). https:\/\/doi.org\/10.1145\/2933575.2934555","DOI":"10.1145\/2933575.2934555"},{"key":"1_CR134","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., et al.: Arch-comp22 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2022). EPiC Series in Computing, vol.\u00a090, pp. 142\u2013184. EasyChair (2022). https:\/\/doi.org\/10.29007\/wfgr","DOI":"10.29007\/wfgr"},{"key":"1_CR135","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., Althoff, M., Forets, M., Johnson, T.T., Ladner, T., Schilling, C.: Arch-comp23 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2023). EPiC Series in Computing, vol.\u00a096, pp. 89\u2013125. EasyChair (2023). https:\/\/doi.org\/10.29007\/x38n. https:\/\/easychair.org\/publications\/paper\/Vfq4b","DOI":"10.29007\/x38n"},{"key":"1_CR136","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-031-37703-7_19","volume-title":"Computer Aided Verification (CAV)","author":"DM Lopez","year":"2023","unstructured":"Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: the neural network verification tool. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13965, pp. 397\u2013412. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_19"},{"key":"1_CR137","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., et al.: Arch-comp19 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: ARCH 2019. International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a061, pp. 103\u2013119. EasyChair (2019). https:\/\/doi.org\/10.29007\/rgv8","DOI":"10.29007\/rgv8"},{"key":"1_CR138","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2022.101303","volume":"47","author":"H Ma","year":"2023","unstructured":"Ma, H., Blom, H.A.: Interacting particle system based estimation of reach probability of general stochastic hybrid systems. Nonlinear Anal. Hybrid Syst 47, 101303 (2023)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"1_CR139","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_1","volume-title":"Computer Aided Verification (CAV)","author":"R Majumdar","year":"2023","unstructured":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.K., Soudjani, S.: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13966. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_1"},{"key":"1_CR140","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Mallik, K., Soudjani, S.: Symbolic controller synthesis for b\u00fcchi specifications on stochastic systems. In: International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2020)","DOI":"10.1145\/3365365.3382214"},{"key":"1_CR141","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"1_CR142","doi-asserted-by":"crossref","unstructured":"Menghi, C., Nejati, S., Briand, L., Isasi\u00a0Parache, Y.: Approximation-refinement testing of compute-intensive cyber-physical models: an approach based on system identification. In: International Conference on Software Engineering (ICSE). IEEE\/ACM (2020)","DOI":"10.1145\/3377811.3380370"},{"key":"1_CR143","doi-asserted-by":"publisher","unstructured":"Mitsch, S.: Implicit and explicit proof management in keymaera X. In: Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24\u201325 May 2021, pp. 53\u201367 (2021). https:\/\/doi.org\/10.4204\/EPTCS.338.8","DOI":"10.4204\/EPTCS.338.8"},{"key":"1_CR144","doi-asserted-by":"publisher","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.) 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21). EPiC Series in Computing, vol.\u00a080, pp. 120\u2013132. EasyChair (2021). https:\/\/doi.org\/10.29007\/35cf","DOI":"10.29007\/35cf"},{"key":"1_CR145","doi-asserted-by":"crossref","unstructured":"Mitsch, S., y\u00a0Munive, J.J.H., Jin, X., Zhan, B., Wang, S., Zhan, N.: ARCH-COMP20 category report: hybrid systems theorem proving. In: ARCH. EPiC Series in Computing, vol.\u00a074, pp. 153\u2013174. EasyChair (2020)","DOI":"10.29007\/bdq9"},{"issue":"1\u20132","key":"1_CR146","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-016-0241-z","volume":"49","author":"S Mitsch","year":"2016","unstructured":"Mitsch, S., Platzer, A.: Modelplex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1\u20132), 33\u201374 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0241-z","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR147","doi-asserted-by":"publisher","unstructured":"Mitsch, S., Sheng, H., Zhan, B., Wang, S., Foster, S., Munive, J.J.H.Y.: Arch-comp23 category report: hybrid systems theorem proving. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23). EPiC Series in Computing, vol.\u00a096, pp. 170\u2013188. EasyChair (2023). https:\/\/doi.org\/10.29007\/57g4","DOI":"10.29007\/57g4"},{"key":"1_CR148","doi-asserted-by":"publisher","unstructured":"Mitsch, S., et al.: Arch-comp22 category report: hybrid systems theorem proving. In: Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J. (eds.) Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2022). EPiC Series in Computing, vol.\u00a090, pp. 185\u2013203. EasyChair (2022). https:\/\/doi.org\/10.29007\/4lxf","DOI":"10.29007\/4lxf"},{"issue":"4","key":"1_CR149","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1016\/j.ifacol.2021.04.060","volume":"53","author":"MS Mufid","year":"2020","unstructured":"Mufid, M.S., Adzkiya, D., Abate, A.: Symbolic reachability analysis of high dimensional max-plus linear systems. IFAC-PapersOnLine 53(4), 459\u2013465 (2020). https:\/\/doi.org\/10.1016\/j.ifacol.2021.04.060","journal-title":"IFAC-PapersOnLine"},{"key":"1_CR150","unstructured":"y\u00a0Munive, J.J.H.: Verification components for hybrid systems. Arch. Formal Proofs 2019 (2019). https:\/\/www.isa-afp.org\/entries\/Hybrid_Systems_VCs.html"},{"key":"1_CR151","unstructured":"NNFal (2023). https:\/\/gitlab.com\/Atanukundu\/NNFal"},{"key":"1_CR152","unstructured":"Peltom\u00e4ki, J., Porres, I.: Requirement falsification for cyber-physical systems using generative models. arXiv preprint arXiv:2310.20493 (2023)"},{"key":"1_CR153","doi-asserted-by":"crossref","unstructured":"Pilch, C., Remke, A.: HYPEG: statistical model checking for hybrid petri nets: tool paper. In: International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2017, pp. 186\u2013191. ACM (2017)","DOI":"10.1145\/3150928.3150956"},{"issue":"2","key":"1_CR154","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)","journal-title":"J. Autom. Reason."},{"key":"1_CR155","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":"1_CR156","doi-asserted-by":"publisher","unstructured":"Qian, M., Mitsch, S.: Reward shaping from hybrid systems models in reinforcement learning. In: NASA Formal Methods - International Symposium (NFM), pp. 122\u2013139 (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_8","DOI":"10.1007\/978-3-031-33170-1_8"},{"issue":"1","key":"1_CR157","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., Ar\u00e9chiga, 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":"1_CR158","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-26287-1_1","volume-title":"Hardware and Software: Verification and Testing","author":"R Ray","year":"2015","unstructured":"Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., Grosu, R.: XSpeed: accelerating reachability analysis on multi-core processors. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 3\u201318. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26287-1_1"},{"key":"1_CR159","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-319-99154-2_24","volume-title":"Quantitative Evaluation of Systems","author":"M Salamati","year":"2018","unstructured":"Salamati, M., Soudjani, S., Majumdar, R.: Approximate time bounded reachability for CTMCs and CTMDPs: a lyapunov approach. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 389\u2013406. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_24"},{"key":"1_CR160","unstructured":"Alexandre\u00a0dit Sandretto, J., Chapoutot, A.: Validated explicit and implicit Runge-Kutta methods. Reliable Comput. Electron. Edition 22 (2016)"},{"key":"1_CR161","doi-asserted-by":"crossref","unstructured":"Schupp, S., Abraham, E., Ben Makhlouf, I., Kowalewski, S.: HyPro: a C++ library for state set representations for hybrid systems reachability analysis. In: Proceedings of the NASA Formal Methods Symposium, pp. 288\u2013294 (2017)","DOI":"10.1007\/978-3-319-57288-8_20"},{"key":"1_CR162","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-031-27481-7_11","volume-title":"Formal Methods","author":"H Sheng","year":"2023","unstructured":"Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: practical verification of hybrid systems using hoare logic. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 160\u2013178. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_11"},{"key":"1_CR163","doi-asserted-by":"crossref","unstructured":"Shmarov, F., Zuliani, P.: ProbReach: verified probabilistic $$\\delta $$-reachability for stochastic hybrid systems. In: HSCC, pp. 134\u2013139. ACM (2015)","DOI":"10.1145\/2728606.2728625"},{"key":"1_CR164","unstructured":"Sidrane, C., Kochenderfer, M.J.: OVERT: verification of nonlinear dynamical systems with neural network controllers via overapproximation. In: Safe Machine Learning Workshop at ICLR (2019)"},{"issue":"1\u20132","key":"1_CR165","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-020-00355-z","volume":"58","author":"A Sogokon","year":"2021","unstructured":"Sogokon, A., Mitsch, S., Tan, Y.K., Cordwell, K., Platzer, A.: Pegasus: sound continuous invariant generation. Formal Methods Syst. Des. 58(1\u20132), 5\u201341 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00355-z","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR166","doi-asserted-by":"crossref","unstructured":"Soudjani, S., Gevaerts, C., Abate, A.: FAUST$$^2$$: formal abstractions of uncountable-STate STochastic processes. In: TACAS, vol.\u00a015, pp. 272\u2013286 (2015)","DOI":"10.1007\/978-3-662-46681-0_23"},{"key":"1_CR167","doi-asserted-by":"publisher","unstructured":"Strauss, M., Mitsch, S.: Slow down, move over: a case study in formal verification, refinement, and testing of the responsibility-sensitive safety model for self-driving cars. In: Tests and Proofs - International Conference (TAP), pp. 149\u2013167 (2023). https:\/\/doi.org\/10.1007\/978-3-031-38828-6_9","DOI":"10.1007\/978-3-031-38828-6_9"},{"key":"1_CR168","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Mitsch, S., Platzer, A.: Verifying switched system stability with logic. In: ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 2:1\u20132:11 (2022). https:\/\/doi.org\/10.1145\/3501710.3519541","DOI":"10.1145\/3501710.3519541"},{"key":"1_CR169","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-85248-1_15","volume-title":"Formal Methods for Industrial Critical Systems","author":"Q Thibeault","year":"2021","unstructured":"Thibeault, Q., Anderson, J., Chandratre, A., Pedrielli, G., Fainekos, G.: PSY-TaLiRo: a python toolbox for\u00a0search-based test generation for\u00a0cyber-physical systems. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 223\u2013231. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_15"},{"key":"1_CR170","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"1_CR171","doi-asserted-by":"publisher","unstructured":"Van\u00a0Huijgevoort, B., Sch\u00f6n, O., Soudjani, S., Haesaert, S.: Syscore: synthesis via stochastic coupling relations. In: International Conference on Hybrid Systems: Computation and Control. HSCC 2023. ACM (2023). https:\/\/doi.org\/10.1145\/3575870.3587123","DOI":"10.1145\/3575870.3587123"},{"key":"1_CR172","doi-asserted-by":"crossref","unstructured":"Vinod, A.P., Gleason, J.D., Oishi, M.M.: Sreachtools: a MATLAB stochastic reachability toolbox. In: ACM International Conference on Hybrid Systems: Computation and Control, pp. 33\u201338 (2019)","DOI":"10.1145\/3302504.3311809"},{"key":"1_CR173","doi-asserted-by":"publisher","unstructured":"Waga, M.: Falsification of cyber-physical systems with robustness-guided black-box checking. In: International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 11:1\u201311:13. ACM (2020).https:\/\/doi.org\/10.1145\/3365365.3382193","DOI":"10.1145\/3365365.3382193"},{"key":"1_CR174","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":"1_CR175","doi-asserted-by":"publisher","unstructured":"Wetzlinger, M., Kochdumper, N., Althoff, M.: Adaptive parameter tuning for reachability analysis of linear systems. In: IEEE Conference on Decision and Control, pp. 5145\u20135152 (2020). https:\/\/doi.org\/10.1109\/CDC42340.2020.9304431","DOI":"10.1109\/CDC42340.2020.9304431"},{"issue":"12","key":"1_CR176","doi-asserted-by":"publisher","first-page":"7771","DOI":"10.1109\/TAC.2023.3292008","volume":"68","author":"M Wetzlinger","year":"2023","unstructured":"Wetzlinger, M., Kochdumper, N., Bak, S., Althoff, M.: Fully automated verification of linear systems using inner and outer approximations of reachable sets. IEEE Trans. Autom. Control 68(12), 7771\u20137786 (2023). https:\/\/doi.org\/10.1109\/TAC.2023.3292008","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR177","doi-asserted-by":"publisher","unstructured":"Wetzlinger, M., Kochdumper, N., Bak, S., Althoff, M.: Fully-automated verification of linear systems using reachability analysis with support functions. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control (2023). https:\/\/doi.org\/10.1145\/3575870.3587121","DOI":"10.1145\/3575870.3587121"},{"key":"1_CR178","doi-asserted-by":"publisher","unstructured":"Wetzlinger, M., Kulmburg, A., Althoff, M.: Adaptive parameter tuning for reachability analysis of nonlinear systems. In: International Conference on Hybrid Systems: Computation and Control. HSCC 2021. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3447928.3456643","DOI":"10.1145\/3447928.3456643"},{"key":"1_CR179","doi-asserted-by":"publisher","unstructured":"Wetzlinger, M., Kulmburg, A., Le Penven, A., Althoff, M.: Adaptive reachability algorithms for nonlinear systems using abstraction error analysis. Nonlinear Anal. Hybrid Syst. 46 (2022).https:\/\/doi.org\/10.1016\/j.nahs.2022.101252","DOI":"10.1016\/j.nahs.2022.101252"},{"key":"1_CR180","doi-asserted-by":"publisher","unstructured":"Winter, S., et al.: A retrospective study of one decade of artifact evaluations. In: ESEC\/FSE 2022: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 145\u2013156. ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3549172","DOI":"10.1145\/3540250.3549172"},{"issue":"12","key":"1_CR181","doi-asserted-by":"publisher","first-page":"2823","DOI":"10.1109\/TSE.2020.2969178","volume":"47","author":"Y Yamagata","year":"2021","unstructured":"Yamagata, Y., Liu, S., Akazaki, T., Duan, Y., Hao, J.: Falsification of cyber-physical systems using deep reinforcement learning. IEEE Trans. Software Eng. 47(12), 2823\u20132840 (2021). https:\/\/doi.org\/10.1109\/TSE.2020.2969178","journal-title":"IEEE Trans. Software Eng."},{"key":"1_CR182","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/978-3-030-81685-8_29","volume-title":"Computer Aided Verification","author":"Z Zhang","year":"2021","unstructured":"Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 595\u2013618. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_29"},{"key":"1_CR183","unstructured":"zlscheck (2023). https:\/\/github.com\/ismailbennani\/zlscheck"}],"container-title":["Lecture Notes in Computer Science","TOOLympics Challenge 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67695-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:13:17Z","timestamp":1750842797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67695-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,1]]},"ISBN":["9783031676949","9783031676956"],"references-count":183,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67695-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,1]]},"assertion":[{"value":"1 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}