{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:51:24Z","timestamp":1767984684120,"version":"3.49.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-10794-7_13","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:21Z","timestamp":1763189001000},"page":"248-267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From Zonotopes to\u00a0Proof Certificates: A Formal Pipeline for\u00a0Safe Control Envelopes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-5530-3256","authenticated-orcid":false,"given":"Jonathan","family":"Hellwig","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4335-9342","authenticated-orcid":false,"given":"Lukas","family":"Sch\u00e4fer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1567-3948","authenticated-orcid":false,"given":"Long","family":"Qian","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3733-842X","authenticated-orcid":false,"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Ahmadi, A.A., Hall, G., Papachristodoulou, A., Saunderson, J., Zheng, Y.: Improving efficiency and scalability of sum of squares optimization: Recent advances and limitations. In: IEEE Conference on Decision and Control, pp. 453\u2013462 (2017). https:\/\/doi.org\/10.1109\/CDC.2017.8263706","DOI":"10.1109\/CDC.2017.8263706"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Althoff, M., Frehse, G.: Combining zonotopes and support functions for efficient reachability analysis of linear systems. In: Proceedings of the 55th IEEE Conference on Decision and Control, pp. 7439\u20137446 (2016). https:\/\/doi.org\/10.1109\/CDC.2016.7799418","DOI":"10.1109\/CDC.2016.7799418"},{"issue":"1","key":"13_CR3","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(1), 369\u2013395 (2021). https:\/\/doi.org\/10.1146\/annurev-control-071420-081941","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Althoff, M., Krogh, B.H.: Zonotope bundles for the efficient computation of reachable sets. In: Proceedings of the 50th IEEE Conference on Decision and Control, pp. 6814\u20136821 (2011). https:\/\/doi.org\/10.1109\/CDC.2011.6160872","DOI":"10.1109\/CDC.2011.6160872"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Althoff, M.: An introduction to CORA 2015. In: ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015). https:\/\/doi.org\/10.29007\/zbkv","DOI":"10.29007\/zbkv"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Althoff, M., Forets, M., Schilling, C., Wetzlinger, M.: ARCH-COMP24 category report: continuous and hybrid systems with linear continuous dynamics. In: Frehse, G., Althoff, M. (eds.) Proceedings of the 11th International Workshop on Applied Verification for Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a0103, pp. 15\u201338. EasyChair (2024). https:\/\/doi.org\/10.29007\/7xf3","DOI":"10.29007\/7xf3"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: theory and applications. In: European Control Conference, pp. 3420\u20133431 (2019). https:\/\/doi.org\/10.23919\/ECC.2019.8796030","DOI":"10.23919\/ECC.2019.8796030"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Ar\u00e9chiga, N., Krogh, B.: Using verified control envelopes for safe controller design. In: 2014 American Control Conference, pp. 2918\u20132923 (2014). https:\/\/doi.org\/10.1109\/ACC.2014.6859307","DOI":"10.1109\/ACC.2014.6859307"},{"issue":"4","key":"13_CR9","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1016\/j.sysconle.2012.01.004","volume":"61","author":"MA Ben Sassi","year":"2012","unstructured":"Ben Sassi, M.A., Girard, A.: Controller synthesis for robust invariance of polynomial dynamical systems using linear programming. Syst. Control Lett. 61(4), 506\u2013512 (2012). https:\/\/doi.org\/10.1016\/j.sysconle.2012.01.004","journal-title":"Syst. Control Lett."},{"issue":"5","key":"13_CR10","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1109\/TAC.1972.1100085","volume":"17","author":"D Bertsekas","year":"1972","unstructured":"Bertsekas, D.: Infinite time reachability of state-space regions by using feedback control. IEEE Trans. Autom. Control 17(5), 604\u2013613 (1972). https:\/\/doi.org\/10.1109\/TAC.1972.1100085","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"13_CR11","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(4), 361\u2013369 (1998). https:\/\/doi.org\/10.1023\/A:1024467732637","journal-title":"Reliable Comput."},{"issue":"11","key":"13_CR12","doi-asserted-by":"publisher","first-page":"1747","DOI":"10.1016\/S0005-1098(99)00113-2","volume":"35","author":"F Blanchini","year":"1999","unstructured":"Blanchini, F.: Set invariance in control. Automatica 35(11), 1747\u20131767 (1999)","journal-title":"Automatica"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"2910","DOI":"10.1109\/LRA.2019.2923099","volume":"4","author":"R Bohrer","year":"2019","unstructured":"Bohrer, R., Tan, Y.K., Mitsch, S., Sogokon, A., Platzer, A.: A formal safety net for waypoint-following in ground robots. IEEE Robot. Autom. Lett. 4(3), 2910\u20132917 (2019). https:\/\/doi.org\/10.1109\/LRA.2019.2923099","journal-title":"IEEE Robot. Autom. Lett."},{"issue":"9","key":"13_CR14","doi-asserted-by":"publisher","first-page":"1583","DOI":"10.1016\/j.automatica.2005.04.015","volume":"41","author":"J Bravo","year":"2005","unstructured":"Bravo, J., Limon, D., Alamo, T., Camacho, E.: On the computation of invariant sets for constrained nonlinear systems: an interval arithmetic approach. Automatica 41(9), 1583\u20131589 (2005). https:\/\/doi.org\/10.1016\/j.automatica.2005.04.015","journal-title":"Automatica"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Brown, S., Khajenejad, M., Yong, S.Z., Mart\u00ednez, S.: Computing controlled invariant sets of nonlinear control-affine systems. In: IEEE Conference on Decision and Control, pp. 7830\u20137836 (2023). https:\/\/doi.org\/10.1109\/CDC49753.2023.10383613","DOI":"10.1109\/CDC49753.2023.10383613"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Chen, M., Tomlin, C.J.: Hamilton\u2013Jacobi reachability: some recent theoretical advances and applications in unmanned airspace management. Annu. Rev. Control Robot. Auton. Syst. 1, 333\u2013358 (2018). https:\/\/doi.org\/10.1146\/annurev-control-060117-104941","DOI":"10.1146\/annurev-control-060117-104941"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Chen, W.H., O\u2019Reilly, J., Ballance, D.: On the terminal region of model predictive control for non-linear systems with input\/state constraints. Int. J. Adapt. Control Signal Process. 17, 195\u2013207 (2003). https:\/\/doi.org\/10.1002\/acs.731","DOI":"10.1002\/acs.731"},{"key":"13_CR18","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":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"issue":"8","key":"13_CR20","doi-asserted-by":"publisher","first-page":"1334","DOI":"10.1016\/j.automatica.2010.05.007","volume":"46","author":"M Fiacchini","year":"2010","unstructured":"Fiacchini, M., Alamo, T., Camacho, E.: On the computation of convex robust control invariant sets for nonlinear systems. Automatica 46(8), 1334\u20131338 (2010). https:\/\/doi.org\/10.1016\/j.automatica.2010.05.007","journal-title":"Automatica"},{"key":"13_CR21","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":"13_CR22","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":"13_CR23","doi-asserted-by":"publisher","unstructured":"Geretti, L., et al.: ARCH-COMP24 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse, G., Althoff, M. (eds.) Proceedings of the 11th International Workshop on Applied Verification for Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a0103, pp. 39\u201363. EasyChair (2024). https:\/\/doi.org\/10.29007\/21ch","DOI":"10.29007\/21ch"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11730637_22","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2006","unstructured":"Girard, A., Pappas, G.J.: Verification using simulation. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 272\u2013286. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_22"},{"issue":"2","key":"13_CR25","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1109\/LCSYS.2020.3002476","volume":"5","author":"F Gruber","year":"2021","unstructured":"Gruber, F., Althoff, M.: Computing safe sets of linear sampled-data systems. IEEE Control Syst. Lett. 5(2), 385\u2013390 (2021). https:\/\/doi.org\/10.1109\/LCSYS.2020.3002476","journal-title":"IEEE Control Syst. Lett."},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Gruber, F., Althoff, M.: Scalable robust output feedback MPC of linear sampled-data systems. In: IEEE Conference on Decision and Control, pp. 2563\u20132570 (2021). https:\/\/doi.org\/10.1109\/CDC45484.2021.9683384","DOI":"10.1109\/CDC45484.2021.9683384"},{"issue":"1","key":"13_CR27","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/LCSYS.2018.2849714","volume":"3","author":"A Gupta","year":"2019","unstructured":"Gupta, A., Falcone, P.: Full-complexity characterization of control-invariant domains for systems with uncertain parameter dependence. IEEE Control Syst. Lett. 3(1), 19\u201324 (2019). https:\/\/doi.org\/10.1109\/LCSYS.2018.2849714","journal-title":"IEEE Control Syst. Lett."},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Hellwig, J., Sch\u00e4fer, L., Qian, L., Platzer, A., Althoff, M.: From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes (2025). https:\/\/doi.org\/10.48550\/arXiv.2509.20301","DOI":"10.48550\/arXiv.2509.20301"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Jeannin, J.B., et al.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: 2015 International Conference on Embedded Software (EMSOFT), pp. 127\u2013136 (2015). https:\/\/doi.org\/10.1109\/EMSOFT.2015.7318268","DOI":"10.1109\/EMSOFT.2015.7318268"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Kabra, A., Laurent, J., Mitsch, S., Platzer, A.: CESAR: control envelope synthesis via angelic refinements. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 144\u2013164. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_9","DOI":"10.1007\/978-3-031-57246-3_9"},{"issue":"11","key":"13_CR31","doi-asserted-by":"publisher","first-page":"4409","DOI":"10.1109\/TCAD.2022.3197690","volume":"41","author":"A Kabra","year":"2022","unstructured":"Kabra, A., Mitsch, S., Platzer, A.: Verified train controllers for the federal railroad administration train kinematics model: balancing competing brake and track forces. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4409\u20134420 (2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197690","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"5","key":"13_CR32","doi-asserted-by":"publisher","first-page":"2944","DOI":"10.1137\/130914565","volume":"52","author":"M Korda","year":"2014","unstructured":"Korda, M., Henrion, D., Jones, C.N.: Convex computation of the maximum controlled invariant set for polynomial control systems. SIAM J. Control. Optim. 52(5), 2944\u20132969 (2014). https:\/\/doi.org\/10.1137\/130914565","journal-title":"SIAM J. Control. Optim."},{"key":"13_CR33","unstructured":"Krstic, M., Kanellakopoulos, I., Kokotovic, P.V.: Nonlinear and Adaptive Control Design, 1 edn. Wiley-Interscience (1995)"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Kulmburg, A., Schafer, L., Althoff, M.: Approximability of the containment problem for zonotopes and ellipsotopes. IEEE Trans. Autom. Control 1\u201316 (2025). https:\/\/doi.org\/10.1109\/TAC.2025.3583624","DOI":"10.1109\/TAC.2025.3583624"},{"issue":"20","key":"13_CR35","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.ifacol.2018.11.006","volume":"51","author":"M Lazar","year":"2018","unstructured":"Lazar, M., Tetteroo, M.: Computation of terminal costs and sets for discrete\u2013time nonlinear MPC. IFAC-PapersOnLine 51(20), 141\u2013146 (2018). https:\/\/doi.org\/10.1016\/j.ifacol.2018.11.006","journal-title":"IFAC-PapersOnLine"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Mitchell, I.M., Yeh, J., Laine, F.J., Tomlin, C.J.: Ensuring safety for sampled data systems: an efficient algorithm for filtering potentially unsafe input signals. In: IEEE Conference on Decision and Control, pp. 7431\u20137438 (2016). https:\/\/doi.org\/10.1109\/CDC.2016.7799417","DOI":"10.1109\/CDC.2016.7799417"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. Other Titles in Applied Mathematics, Society for Industrial and Applied Mathematics (2009). https:\/\/doi.org\/10.1137\/1.9780898717716","DOI":"10.1137\/1.9780898717716"},{"issue":"2","key":"13_CR38","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219\u2013265 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reason."},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0","DOI":"10.1007\/978-3-319-63588-0"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Platzer, A., Qian, L.: Axiomatization of compact initial value problems: open properties. J. ACM. https:\/\/doi.org\/10.1145\/3763228","DOI":"10.1145\/3763228"},{"issue":"7","key":"13_CR41","doi-asserted-by":"publisher","first-page":"1599","DOI":"10.1109\/TAC.2010.2042341","volume":"55","author":"SV Rakovic","year":"2010","unstructured":"Rakovic, S.V., Baric, M.: Parameterized robust control invariant sets for linear systems: theoretical advances and computational remarks. IEEE Trans. Autom. Control 55(7), 1599\u20131614 (2010). https:\/\/doi.org\/10.1109\/TAC.2010.2042341","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"13_CR42","doi-asserted-by":"publisher","first-page":"3057","DOI":"10.1016\/j.ifacol.2017.08.675","volume":"50","author":"S Rakovi\u0107","year":"2017","unstructured":"Rakovi\u0107, S., Fontes, F., Kolmanovsky, I.: Reachability and invariance for linear sampled\u2013data systems. IFAC-PapersOnLine 50(1), 3057\u20133062 (2017). https:\/\/doi.org\/10.1016\/j.ifacol.2017.08.675","journal-title":"IFAC-PapersOnLine"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Rauscher, M., Kimmel, M., Hirche, S.: Constrained robot control using control barrier functions. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 279\u2013285 (2016). https:\/\/doi.org\/10.1109\/IROS.2016.7759067","DOI":"10.1109\/IROS.2016.7759067"},{"key":"13_CR44","unstructured":"Rawlings, J.B., Mayne, D.Q., Diehl, M.M.: Model Predictive Control: Theory, Computation, and Design. Nob Hill Publishing, LLC (2022)"},{"issue":"7","key":"13_CR45","doi-asserted-by":"publisher","first-page":"3665","DOI":"10.1109\/TAC.2017.2672859","volume":"62","author":"M Rungger","year":"2017","unstructured":"Rungger, M., Tabuada, P.: Computing robust controlled invariant sets of linear systems. IEEE Trans. Autom. Control 62(7), 3665\u20133670 (2017). https:\/\/doi.org\/10.1109\/TAC.2017.2672859","journal-title":"IEEE Trans. Autom. Control"},{"key":"13_CR46","doi-asserted-by":"publisher","unstructured":"Sadraddini, S., Tedrake, R.: Linear encodings for polytope containment problems. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 4367\u20134372 (2019). https:\/\/doi.org\/10.1109\/CDC40024.2019.9029363","DOI":"10.1109\/CDC40024.2019.9029363"},{"issue":"2","key":"13_CR47","doi-asserted-by":"publisher","first-page":"755","DOI":"10.1109\/TAC.2023.3275305","volume":"69","author":"L Sch\u00e4fer","year":"2024","unstructured":"Sch\u00e4fer, L., Gruber, F., Althoff, M.: Scalable computation of robust control invariant sets of nonlinear systems. IEEE Trans. Autom. Control 69(2), 755\u2013770 (2024). https:\/\/doi.org\/10.1109\/TAC.2023.3275305","journal-title":"IEEE Trans. Autom. Control"},{"key":"13_CR48","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, L., Althoff, M.: Computing robust control invariant sets of nonlinear systems using polynomial controller synthesis. In: Proceedings of the American Control Conference (2024). https:\/\/doi.org\/10.23919\/ACC60939.2024.10644939","DOI":"10.23919\/ACC60939.2024.10644939"},{"key":"13_CR49","doi-asserted-by":"publisher","unstructured":"Sch\u00fcrmann, B., Kochdumper, N., Althoff, M.: Reachset model predictive control for disturbed nonlinear systems. In: 2018 IEEE Conference on Decision and Control (CDC), pp. 3463\u20133470 (2018). https:\/\/doi.org\/10.1109\/CDC.2018.8619781","DOI":"10.1109\/CDC.2018.8619781"},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Selvaraj, Y., Krook, J., Ahrendt, W., Fabian, M.: On proving that an unsafe controller is not proven safe. J. Log. Algebraic Methods Program. 137, 100939 (2024). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100939","DOI":"10.1016\/j.jlamp.2023.100939"},{"key":"13_CR51","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Mitsch, S., Platzer, A.: Verifying switched system stability with logic. In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2022, pp. 1\u201311. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3501710.3519541","DOI":"10.1145\/3501710.3519541"},{"key":"13_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-030-72013-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"YK Tan","year":"2021","unstructured":"Tan, Y.K., Platzer, A.: Deductive stability proofs for ordinary differential equations. In: TACAS 2021. LNCS, vol. 12652, pp. 181\u2013199. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_10"},{"key":"13_CR53","doi-asserted-by":"publisher","unstructured":"Wabersich, K.P., Zeilinger, M.N.: Linear model predictive safety certification for learning-based control. In: 2018 IEEE Conference on Decision and Control (CDC), pp. 7130\u20137135 (2018). https:\/\/doi.org\/10.1109\/CDC.2018.8619829","DOI":"10.1109\/CDC.2018.8619829"},{"key":"13_CR54","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":"13_CR55","doi-asserted-by":"publisher","unstructured":"Wetzlinger, M., Kulmburg, A., Althoff, M.: Adaptive parameter tuning for reachability analysis of nonlinear systems. In: Proceedings of the 24th 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"},{"issue":"27","key":"13_CR56","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.ifacol.2015.11.152","volume":"48","author":"X Xu","year":"2015","unstructured":"Xu, X., Tabuada, P., Grizzle, J.W., Ames, A.D.: Robustness of control barrier functions for safety critical control. IFAC-PapersOnLine 48(27), 54\u201361 (2015). https:\/\/doi.org\/10.1016\/j.ifacol.2015.11.152","journal-title":"IFAC-PapersOnLine"},{"issue":"2","key":"13_CR57","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/19M125220X","volume":"59","author":"B Xue","year":"2021","unstructured":"Xue, B., Wang, Q., Zhan, N., Wang, S., She, Z.: Synthesizing robust domains of attraction for state-constrained perturbed polynomial systems. SIAM J. Control. Optim. 59(2), 1083\u20131108 (2021). https:\/\/doi.org\/10.1137\/19M125220X","journal-title":"SIAM J. Control. Optim."},{"key":"13_CR58","doi-asserted-by":"publisher","unstructured":"Xue, B., Wang, Q., Zhan, N., Fr\u00e4nzle, M.: Robust invariant sets generation for state-constrained perturbed polynomial systems. In: International Conference on Hybrid Systems: Computation and Control, pp. 128\u2013137 (2019). https:\/\/doi.org\/10.1145\/3302504.3311810","DOI":"10.1145\/3302504.3311810"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:58:47Z","timestamp":1767967127000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}