{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T21:39:23Z","timestamp":1768340363818,"version":"3.49.0"},"publisher-location":"Cham","reference-count":121,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031067723","type":"print"},{"value":"9783031067730","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_6","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"109-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Reachability Analysis for\u00a0Cyber-Physical Systems: Are We There Yet?"],"prefix":"10.1007","author":[{"given":"Xin","family":"Chen","sequence":"first","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"issue":"12s","key":"6_CR1","first-page":"95","volume":"12","author":"H Abbas","year":"2013","unstructured":"Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embedded Comput. Syst. (TECS) 12(12s), 95 (2013)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"6_CR2","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proceedings of ARCH 2015, EPiC Series in Computer Science, vol. 34, pp. 120\u2013151. EasyChair (2015)"},{"issue":"2","key":"6_CR3","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.nahs.2009.03.009","volume":"4","author":"M Althoff","year":"2010","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Anal. Hybrid Syst 4(2), 233\u2013249 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Annu. Rev. Control Robot. Auton. Syst. 4, 369\u2013395 (2021)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Proceedings of HSCC 2012, pp. 45\u201354. ACM (2012)","DOI":"10.1145\/2185632.2185643"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: Proceedings of CDC 2008, pp. 4042\u20134048. IEEE (2008)","DOI":"10.1109\/CDC.2008.4738704"},{"key":"6_CR7","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107l, F.: Counter-example guided predicate abstraction of hybrid systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 208\u2013223. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_15","DOI":"10.1007\/3-540-36577-X_15"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"7","key":"6_CR12","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"issue":"4","key":"6_CR13","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/37.88585","volume":"11","author":"PJ Antsaklis","year":"1991","unstructured":"Antsaklis, P.J., Passino, K.M., Wang, S.J.: An introduction to autonomous control systems. IEEE Control Syst. Mag. 11(4), 5\u201313 (1991)","journal-title":"IEEE Control Syst. Mag."},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365\u2013370. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_30"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(94)00228-B","volume":"138","author":"E Asarin","year":"1995","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoret. Comput. Sci. 138, 35\u201366 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR16","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Duggirala, P.S., Gerlach, A.R., Potomkin, K.: Reachability of black-box nonlinear systems after Koopman operator linearization. In: Analysis and Design of Hybrid Systems (ADHS), IFAC-PapersOnLine, vol. 54, pp. 253\u2013258. Elsevier (2021)","DOI":"10.1016\/j.ifacol.2021.08.507"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: HyLAA: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of HSCC 2017, pp. 173\u2013178. ACM (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"6_CR19","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: HSCC 2019, pp. 23\u201332. Association for Computing Machinery, New York (2019)","DOI":"10.29007\/b8zr"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1\u20133. ACM, New York (2002)","DOI":"10.1145\/503272.503274"},{"issue":"40","key":"6_CR21","doi-asserted-by":"publisher","first-page":"3625","DOI":"10.1016\/j.tcs.2010.06.005","volume":"411","author":"PC Bell","year":"2010","unstructured":"Bell, P.C., Delvenne, J.-C., Jungers, R.M., Blondel, V.D.: The continuous Skolem-Pisot problem. Theoret. Comput. Sci. 411(40), 3625\u20133634 (2010)","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"6_CR22","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1109\/9.53519","volume":"35","author":"A Benveniste","year":"1990","unstructured":"Benveniste, A., Le Guernic, P.: Hybrid dynamical systems theory and the signal language. IEEE Trans. Autom. Control 35(5), 535\u2013546 (1990)","journal-title":"IEEE Trans. Autom. Control"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Benvenuti, L., et al.: Reachability computation for hybrid systems with Ariadne. In: Proceedings of the 17th IFAC World Congress. IFAC Papers-OnLine (2008)","DOI":"10.3182\/20080706-5-KR-1001.01513"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-33512-9_8","volume-title":"Reachability Problems","author":"L Benvenuti","year":"2012","unstructured":"Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 79\u201391. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33512-9_8"},{"key":"6_CR25","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1023\/A:1024467732637","volume":"4","author":"M Berz","year":"1998","unstructured":"Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Comput. 4, 361\u2013369 (1998)","journal-title":"Reliable Comput."},{"issue":"5\u20136","key":"6_CR26","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. STTT 9(5\u20136), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: Programming Language Design & Implementation, pp. 196\u2013207. ACM Press (2003)","DOI":"10.1145\/780822.781153"},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2914770.2837649","volume":"51","author":"L Cardelli","year":"2016","unstructured":"Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. ACM SIGPLAN Not. 51, 137\u2013150 (2016)","journal-title":"ACM SIGPLAN Not."},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Chen, M., Herbert, S.L., Vashishtha, M.S., Bansal, S., Tomlin, C.J.: Decomposition of reachable sets and tubes for a class of nonlinear systems. arXiv e-prints (2017)","DOI":"10.1109\/TAC.2018.2797194"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Chen, M., Herbert, S., Tomlin, C.: Exact and efficient Hamilton-Jacobi-based guaranteed safety analysis via system decomposition. In: IEEE International Conference on Robotics and Automation (ICRA) (2017). arXiv:1609.05248","DOI":"10.1109\/ICRA.2017.7989015"},{"key":"6_CR31","unstructured":"Chen, X.: Reachability analysis of non-linear hybrid systems using Taylor models. Ph.D. thesis, RWTH Aachen University (2015)"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS 2012), pp. 183\u2013192. IEEE Computer Society (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"6_CR33","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":"6_CR34","unstructured":"Chen, X., Dutta, S., Sankaranarayanan, S.: Formal verification of a multi-basal insulin infusion control model. In: Workshop on Applied Verification of Hybrid Systems (ARCH), p. 16. Easychair (2017)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S.: Decomposed reachability analysis for nonlinear systems. In: IEEE Real Time Systems Symposium (RTSS), pp. 13\u201324. IEEE Press (2016)","DOI":"10.1109\/RTSS.2016.011"},{"key":"6_CR36","unstructured":"Chonev, V., Ouaknine, J., Worrell, J.: On the skolem problem for continuous linear dynamical systems. In: ICALP 2016, LIPIcs, vol. 55, pp. 100:1\u2013100:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-63501-9_8","volume-title":"Numerical Software Verification","author":"Y Chou","year":"2017","unstructured":"Chou, Y., Chen, X., Sankaranarayanan, S.: A study of model-order reduction techniques for verification. In: Abate, A., Boldo, S. (eds.) NSV 2017. LNCS, vol. 10381, pp. 98\u2013113. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63501-9_8"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Chou, Y., Yoon, H., Sankaranarayanan, S.: Predictive runtime monitoring of vehicle models using Bayesian estimation and reachability analysis. In: International Conference on Intelligent Robots and Systems (IROS), pp. 2111\u20132118. IEEE Press (2020)","DOI":"10.1109\/IROS45743.2020.9340755"},{"key":"6_CR39","unstructured":"Chutinan, A., Krogh, B.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of IEEE CDC. IEEE Press (1998)"},{"key":"6_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"6_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 192\u2013207. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_14"},{"key":"6_CR42","unstructured":"Edmund, M., Clarke, O.G., Peled, D.A: Model Checking. MIT Press, Cambridge (1999)"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Coogan, S.: Mixed monotonicity for reachability and safety in dynamical systems. In: 2020 59th IEEE Conference on Decision and Control (CDC), pp. 5074\u20135085. IEEE Press (2020)","DOI":"10.1109\/CDC42340.2020.9304391"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Coogan, S., Arcak, M.: Efficient finite abstraction of mixed monotone systems. In: Girard, A., Sankaranarayanan, S. (eds.) HSCC 2015, pp. 58\u201367. ACM (2015)","DOI":"10.1145\/2728606.2728607"},{"key":"6_CR45","volume-title":"Principles of Abstract Interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: Proceedings of HSCC 2010, pp. 11\u201320. ACM (2010)","DOI":"10.1145\/1755952.1755956"},{"key":"6_CR47","doi-asserted-by":"crossref","unstructured":"Dang, T., Testylier, R.: Hybridization domain construction using curvature estimation. In: Proceedings of HSCC 2011, pp. 123\u2013132. ACM (2011)","DOI":"10.1145\/1967701.1967721"},{"key":"6_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-540-74061-2_27","volume-title":"Static Analysis","author":"D Delmas","year":"2007","unstructured":"Delmas, D., Souyris, J.: Astr\u00e9e: from research to industry. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 437\u2013451. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_27"},{"key":"6_CR49","unstructured":"Donz\u00e9, A.: BreachFlows: simulation-based design with formal requirements for industrial CPS (extended abstract). In: Workshop on Autonomous Systems Design (ASD 2020). OpenAccess Series in Informatics (OASIcs), vol. 79, pp. 5:1\u20135:5 (2020)"},{"key":"6_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_5"},{"key":"6_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-319-41528-4_26","volume-title":"Computer Aided Verification","author":"PS Duggirala","year":"2016","unstructured":"Duggirala, P.S., Viswanathan, M.: Parsimonious, simulation based verification of linear systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 477\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_26"},{"key":"6_CR52","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Ozay, N., Prabhakar, P. (eds.) Proceedings of HSCC 2019, pp. 157\u2013168. ACM (2019)","DOI":"10.1145\/3302504.3311807"},{"key":"6_CR53","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":"6_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-24690-6_13","volume-title":"Software Engineering and Formal Methods","author":"A Eggers","year":"2011","unstructured":"Eggers, A., Ramdani, N., Nedialkov, N., Fr\u00e4nzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 172\u2013187. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_13"},{"key":"6_CR55","doi-asserted-by":"crossref","unstructured":"M. Fr\u00e4nzle, C. Herde, S. Ratschan, T. Schubert, Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. JSAT\u2013J. Satisfiability Boolean Model. Comput. 1, 209\u2013236 (2007). Special Issue on SAT\/CP Integration","DOI":"10.3233\/SAT190012"},{"key":"6_CR56","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., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: 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":"6_CR57","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"6_CR58","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo odes. In: Proceedings of FMCAD 2013, pp. 105\u2013112. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"6_CR59","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: Proceedings of S & P 2018, pp. 3\u201318. IEEE Computer Society (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"6_CR60","first-page":"19","volume":"47","author":"K Ghorbal","year":"2017","unstructured":"Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47, 19\u201343 (2017)","journal-title":"Comput. Lang. Syst. Struct."},{"issue":"1","key":"6_CR61","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1049\/sb:20045019","volume":"1","author":"R Ghosh","year":"2004","unstructured":"Ghosh, R., Tomlin, C.J.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modeling: Delta-Notch protein signaling. IEE Trans. Syst. Biol. 1(1), 170\u2013183 (2004)","journal-title":"IEE Trans. Syst. Biol."},{"key":"6_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291\u2013305. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_19"},{"key":"6_CR63","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":"6_CR64","doi-asserted-by":"crossref","unstructured":"Gollu, A., Varaiya, P.: Hybrid dynamical systems. In: Proceedings of the 28th IEEE Conference on Decision and Control, vol. 3, pp. 2708\u20132712 (1989)","DOI":"10.1109\/CDC.1989.70671"},{"key":"6_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-642-02658-4_40","volume-title":"Computer Aided Verification","author":"C Le Guernic","year":"2009","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540\u2013554. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_40"},{"issue":"2","key":"6_CR66","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods Syst. Des. 11(2), 157\u2013185 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR67","doi-asserted-by":"crossref","unstructured":"Han, Z., Krogh, B.: Reachability analysis of hybrid control systems using reduced-order models. In: Proceedings of the American Control Conference, vol. 2, pp. 1183\u20131189, January 2004","DOI":"10.23919\/ACC.2004.1386733"},{"key":"6_CR68","unstructured":"Harrison, J.: Formal methods at Intel - an overview. In: Proceedings of the Second NASA Formal Methods Symposium (NFM) (2010)"},{"issue":"4","key":"6_CR69","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Trans. 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"6_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: HyTech: the Cornell hybrid technology tool. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 265\u2013293. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60472-3_14"},{"issue":"1","key":"6_CR71","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR72","doi-asserted-by":"crossref","unstructured":"Herde, C., Eggers, A., Franzle, T., Teige, M.: Analysis of hybrid systems using HySAT. In: Third International Conference on Systems 2008. ICONS 2008, pp. 13\u201318. IEEE (2008)","DOI":"10.1109\/ICONS.2008.17"},{"key":"6_CR73","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: ReachNN: reachability analysis of neural-network controlled systems. ACM Trans. Embed. Comput. Syst. 18(5s), 106:1\u2013106:22 (2019)","DOI":"10.1145\/3358228"},{"key":"6_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"6_CR75","doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A., Ganai, M.K.: Model checking C programs using f-soft. In: ICCD, pp. 297\u2013308. IEEE Computer Society (2005)","DOI":"10.1109\/ICCD.2005.77"},{"key":"6_CR76","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verifying the safety of autonomous systems with neural network controllers. ACM Trans. Embed. Comput. Syst. 20(1), 7:1\u20137:26 (2021)","DOI":"10.1145\/3419742"},{"key":"6_CR77","unstructured":"Kapela, T., Mrozek, M., Pilarczyk, P., Wilczak, D., Zgliczy\u0144ski, P.: CAPD - a rigorous toolbox for computer assisted proofs in dynamics. Technical report, Jagiellonian University (2010)"},{"key":"6_CR78","doi-asserted-by":"crossref","unstructured":"Kapinski, J., Deshmukh, J.V., Jin, X., Ito, H., Butts, K.R.: Simulation-guided approaches for verification of automotive powertrain control systems. In: American Control Conference, ACC 2015, Chicago, IL, USA, 1\u20133 July 2015, pp. 4086\u20134095. IEEE (2015)","DOI":"10.1109\/ACC.2015.7171968"},{"key":"6_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"6_CR80","doi-asserted-by":"publisher","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_15","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"6_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-46430-1_19","volume-title":"Hybrid Systems: Computation and Control","author":"AB Kurzhanski","year":"2000","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 202\u2013214. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46430-1_19"},{"key":"6_CR82","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/PL00009858","volume":"13","author":"G Lafferriere","year":"2000","unstructured":"Lafferriere, G., Pappas, G., Sastry, S.: O-minimal hybrid systems. Math. Control Sig. Syst. 13, 1\u201321 (2000)","journal-title":"Math. Control Sig. Syst."},{"key":"6_CR83","doi-asserted-by":"crossref","unstructured":"Guernic, C.L., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250\u2013262 (2010). IFAC World Congress 2008","DOI":"10.1016\/j.nahs.2009.03.002"},{"key":"6_CR84","unstructured":"Lygeros, J.: Lecture notes on hybrid systems (2004). Notes for ENSIETA short course"},{"issue":"3","key":"6_CR85","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/S0005-1098(98)00193-9","volume":"35","author":"J Lygeros","year":"1999","unstructured":"Lygeros, J., Tomlin, C., Sastry, S.: Controllers for reachability specifications for hybrid systems. Automatica 35(3), 349\u2013370 (1999)","journal-title":"Automatica"},{"issue":"2","key":"6_CR86","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1109\/LCSYS.2018.2800125","volume":"2","author":"J Maidens","year":"2018","unstructured":"Maidens, J., Arcak, M.: Exploiting symmetry for discrete-time reachability computations. IEEE Control Syst. Lett. 2(2), 213\u2013217 (2018)","journal-title":"IEEE Control Syst. Lett."},{"key":"6_CR87","unstructured":"Makino, K., Berz, M.: Remainder differential algebras and their applications. In: Berz, M., et al. (eds.) Computational Differentiation: Techniques, Applications, and Tools, pp. 63\u201375. SIAM (1996)"},{"key":"6_CR88","doi-asserted-by":"crossref","unstructured":"Maler, O.: Amir Pnueli and the dawn of hybrid systems. In: Proceedings of the Hybrid Systems: Computation and Control, pp. 293\u2013295. Association for Computing Machinery (2010)","DOI":"10.1145\/1755952.1755953"},{"key":"6_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/BFb0032003","volume-title":"Real-Time: Theory in Practice","author":"O Maler","year":"1992","unstructured":"Maler, O., Manna, Z., Pnueli, A.: Prom timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 447\u2013484. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0032003"},{"key":"6_CR90","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-35713-9","volume-title":"The Koopman Operator in Systems and Control","year":"2020","unstructured":"Mauroy, A., Mezi\u0107, I., Susuki, Y. (eds.): The Koopman Operator in Systems and Control. LNCIS, vol. 484. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-35713-9"},{"key":"6_CR91","doi-asserted-by":"crossref","unstructured":"Meiss, J.D.: Differential Dynamical Systems. SIAM Publishers (2007)","DOI":"10.1137\/1.9780898718232"},{"key":"6_CR92","unstructured":"Mitchell, I.: Toolbox of level-set methods. Technical report, UBC Department of Computer Science Technical Report TR-2007-11 (2007)"},{"key":"6_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-46430-1_27","volume-title":"Hybrid Systems: Computation and Control","author":"I Mitchell","year":"2000","unstructured":"Mitchell, I., Tomlin, C.J.: Level set methods for computation in hybrid systems. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 310\u2013323. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46430-1_27"},{"key":"6_CR94","doi-asserted-by":"publisher","first-page":"2354","DOI":"10.1103\/PhysRevLett.64.2354","volume":"64","author":"C Moore","year":"1990","unstructured":"Moore, C.: Unpredictability and undecidability in dynamical systems. Phys. Rev. Lett. 64, 2354\u20132357 (1990)","journal-title":"Phys. Rev. Lett."},{"key":"6_CR95","series-title":"Design, and Simulation of Systems with Uncertainties, volume 3 of Mathematical Engineering, chapter Mathematical Engineering","first-page":"3","volume-title":"Modeling","author":"NS Nedialkov","year":"2011","unstructured":"Nedialkov, N.S.: Implementing a rigorous ode solver through literate programming. In: Rauh, A., Auer, E. (eds.) Modeling. Design, and Simulation of Systems with Uncertainties, volume 3 of Mathematical Engineering, chapter Mathematical Engineering, pp. 3\u201319. Springer, Berlin Heidelberg (2011)"},{"key":"6_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-57318-6_28","volume-title":"Hybrid Systems","author":"X Nicollin","year":"1993","unstructured":"Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: An approach to the description and analysis of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 149\u2013178. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_28"},{"key":"6_CR97","doi-asserted-by":"crossref","unstructured":"Peleties, P., DeCarlo, R.: A modeling strategy with event structures for hybrid systems. In: Proceedings of the 28th IEEE Conference on Decision and Control, vol. 2, pp. 1308\u20131313 (1989)","DOI":"10.1109\/CDC.1989.70349"},{"key":"6_CR98","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems, 1st edn. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0","DOI":"10.1007\/978-3-319-63588-0"},{"key":"6_CR99","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.: Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. 35(1), 98\u2013120 (2009)","DOI":"10.1007\/s10703-009-0079-8"},{"key":"6_CR100","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":"6_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-540-78929-1_55","volume-title":"Hybrid Systems: Computation and Control","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: Logical verification and systematic parametric analysis in train control. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 646\u2013649. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_55"},{"issue":"2","key":"6_CR102","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10703-015-0225-4","volume":"46","author":"P Prabhakar","year":"2015","unstructured":"Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. Formal Methods Syst. Des. 46(2), 105\u2013134 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0225-4","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"issue":"2","key":"6_CR104","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.nahs.2010.05.010","volume":"5","author":"N Ramdani","year":"2011","unstructured":"Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5(2), 149\u2013162 (2011)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"6_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-540-31954-2_37","volume-title":"Hybrid Systems: Computation and Control","author":"S Ratschan","year":"2005","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573\u2013589. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_37"},{"issue":"4","key":"6_CR106","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1109\/TSMCB.2002.1018763","volume":"32","author":"L Ros","year":"2002","unstructured":"Ros, L., Sabater, A., Thomas, F.: An ellipsoidal calculus based on propagation and fusion. IEEE Trans. Syst. Man Cybern. Part B 32(4), 430\u2013442 (2002)","journal-title":"IEEE Trans. Syst. Man Cybern. Part B"},{"key":"6_CR107","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.nahs.2015.08.006","volume":"19","author":"S Sankaranarayanan","year":"2016","unstructured":"Sankaranarayanan, S.: Change of basis abstractions for non-linear hybrid systems. Nonlinear Anal. Hybrid Syst 19, 107\u2013133 (2016)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"6_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1007\/978-3-030-53288-8_30","volume-title":"Computer Aided Verification","author":"S Sankaranarayanan","year":"2020","unstructured":"Sankaranarayanan, S.: Reachability analysis using message passing over tree decompositions. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 604\u2013628. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_30"},{"key":"6_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78800-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Dang, T., Ivan\u010di\u0107, F.: Symbolic model checking of hybrid systems using template Polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188\u2013202. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_14"},{"issue":"1","key":"6_CR110","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25\u201355 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR111","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-45190-5_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Sibai","year":"2020","unstructured":"Sibai, H., Mokhlesi, N., Fan, C., Mitra, S.: Multi-agent safety verification using symmetry transformations. In: TACAS 2020. LNCS, vol. 12078, pp. 173\u2013190. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_10"},{"key":"6_CR112","doi-asserted-by":"crossref","unstructured":"Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using checkmate. In: ADPM 2000 (2000). http:\/\/www.ece.cmu.edu\/~webk\/checkmate","DOI":"10.1109\/ACC.2000.879487"},{"key":"6_CR113","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: HSCC, pp. 147\u2013156. ACM (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"6_CR114","doi-asserted-by":"publisher","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"6_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-540-24743-2_40","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600\u2013614. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_40"},{"key":"6_CR116","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"},{"issue":"2","key":"6_CR117","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"6_CR118","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-70583-3_12","volume-title":"Automata, Languages and Programming","author":"V Vladimerou","year":"2008","unstructured":"Vladimerou, V., Prabhakar, P., Viswanathan, M., Dullerud, G.: STORMED hybrid systems. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 136\u2013147. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70583-3_12"},{"key":"6_CR119","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Proceedings of USENIX Security 2018, pp. 1599\u20131614. USENIX Association (2018)"},{"key":"6_CR120","unstructured":"Zhao, F.: Automatic analysis and synthesis of controllers for dynamical systems based on phase-space knowledge. Ph.D. thesis (1998)"},{"key":"6_CR121","doi-asserted-by":"crossref","unstructured":"Zutshi, A., Sankaranarayanan, S., Deshmukh, J., Jin, X.: Symbolic-numeric reachability analysis of closed-loop control software. In: Hybrid Systems: Computation and Control (HSCC), pp. 135\u2013144. ACM Press (2016)","DOI":"10.1145\/2883817.2883819"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,25]],"date-time":"2024-09-25T14:24:24Z","timestamp":1727274264000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":121,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"118","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}