{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:22:59Z","timestamp":1762816979537,"version":"build-2065373602"},"publisher-location":"Singapore","reference-count":58,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819542123"},{"type":"electronic","value":"9789819542130"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"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-981-95-4213-0_17","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:17:53Z","timestamp":1762816673000},"page":"305-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantitative Verification for\u00a0Temporal Properties of\u00a0Massive Linear Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-5202-813X","authenticated-orcid":false,"given":"Qing","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1302-2075","authenticated-orcid":false,"given":"Yuntao","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3679-5840","authenticated-orcid":false,"given":"Sung Woo","family":"Choi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5516-2443","authenticated-orcid":false,"given":"Luan Viet","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6946-9526","authenticated-orcid":false,"given":"Hoang-Dung","family":"Tran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"issue":"1","key":"17_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 1\u201339 (2018)","journal-title":"ACM Trans. Model. Comput. Simul. (TOMACS)"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. HSCC 2013, pp. 173\u2013182. Association for Computing Machinery, New York (2013). https:\/\/doi.org\/10.1145\/2461328.2461358","DOI":"10.1145\/2461328.2461358"},{"issue":"2","key":"17_CR3","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). https:\/\/doi.org\/10.1109\/TAC.2019.2906432","journal-title":"IEEE Trans. Autom. Control"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Althoff, M., Krogh, B.H.: Zonotope bundles for the efficient computation of reachable sets. In: 2011 50th IEEE Conference on Decision and Control and European Control Conference, pp. 6814\u20136821 (2011). https:\/\/doi.org\/10.1109\/CDC.2011.6160872","DOI":"10.1109\/CDC.2011.6160872"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Angelopoulos, A.N., Bates, S., et\u00a0al.: Conformal prediction: a gentle introduction. Found. Trends\u00ae Mach. Learn. 16(4), 494\u2013591 (2023)","DOI":"10.1561\/2200000101"},{"key":"17_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"17_CR7","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":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/978-3-662-54577-5_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bak","year":"2017","unstructured":"Bak, S., Duggirala, P.S.: Rigorous simulation-based analysis of linear hybrid systems. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 555\u2013572. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_32"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-319-63387-9_20","volume-title":"Computer Aided Verification","author":"S Bak","year":"2017","unstructured":"Bak, S., Duggirala, P.S.: Simulation-equivalent reachability of large linear systems with inputs. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 401\u2013420. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_20"},{"key":"17_CR10","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"},{"issue":"1","key":"17_CR11","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1111\/rssb.12162","volume":"79","author":"ZI Botev","year":"2017","unstructured":"Botev, Z.I.: The normal law under linear restrictions: simulation and estimation via minimax tilting. J. R. Stat. Soc. Ser. B (Stat. Methodol.) 79(1), 125\u2013148 (2017)","journal-title":"J. R. Stat. Soc. Ser. B (Stat. Methodol.)"},{"key":"17_CR12","doi-asserted-by":"publisher","DOI":"10.1145\/3627991","author":"SW Choi","year":"2023","unstructured":"Choi, S.W., Ivashchenko, M., Nguyen, L.V., Tran, H.D.: Reachability analysis of sigmoidal neural networks. ACM Trans. Embed. Comput. Syst. (2023). https:\/\/doi.org\/10.1145\/3627991. just Accepted","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Choi, S.W., et al.: Reachability analysis of recurrent neural networks. Nonlinear Analysis: Hybrid Systems (2025)","DOI":"10.1016\/j.nahs.2025.101581"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_4"},{"issue":"2","key":"17_CR15","first-page":"128","volume":"17","author":"T Dang","year":"2012","unstructured":"Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliab. Comput. 17(2), 128\u2013152 (2012)","journal-title":"Reliab. Comput."},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"issue":"1","key":"17_CR17","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods Syst. Des. 51(1), 5\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0286-7","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"17_CR20","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"},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3150\/21-BEJ1447","volume":"29","author":"M Fontana","year":"2023","unstructured":"Fontana, M., Zeni, G., Vantini, S.: Conformal prediction: a unified review of theory and new challenges. Bernoulli 29(1), 1\u201323 (2023)","journal-title":"Bernoulli"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Frehse, G., Ray, R.: Flowpipe-guard intersection for reachability computations with support functions*. IFAC Proceedings Volumes 45(9), 94\u2013101 (2012). https:\/\/doi.org\/10.3182\/20120606-3-NL-3011.00053, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1474667015371809. 4th IFAC Conference on Analysis and Design of Hybrid Systems","DOI":"10.3182\/20120606-3-NL-3011.00053"},{"issue":"5","key":"17_CR23","doi-asserted-by":"publisher","first-page":"1236","DOI":"10.1137\/0913071","volume":"13","author":"E Gallopoulos","year":"1992","unstructured":"Gallopoulos, E., Saad, Y.: Efficient solution of parabolic equations by Krylov approximation methods. SIAM J. Sci. Stat. Comput. 13(5), 1236\u20131264 (1992)","journal-title":"SIAM J. Sci. Stat. Comput."},{"key":"17_CR24","doi-asserted-by":"publisher","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo odes. In: 2013 Formal Methods in Computer-Aided Design, pp. 105\u2013112 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679398","DOI":"10.1109\/FMCAD.2013.6679398"},{"issue":"10","key":"17_CR25","doi-asserted-by":"publisher","first-page":"5071","DOI":"10.1109\/TAC.2021.3118335","volume":"67","author":"Y Gao","year":"2021","unstructured":"Gao, Y., Abate, A., Jiang, F.J., Giacobbe, M., Xie, L., Johansson, K.H.: Temporal logic trees for model checking and control synthesis of uncertain discrete-time systems. IEEE Trans. Autom. Control 67(10), 5071\u20135086 (2021)","journal-title":"IEEE Trans. Autom. Control"},{"key":"17_CR26","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":"17_CR27","doi-asserted-by":"publisher","unstructured":"Girard, A., Guernic, C.L.: Efficient reachability analysis for linear systems using support functions. IFAC Proceedings Volumes 41(2), 8966\u20138971 (2008). https:\/\/doi.org\/10.3182\/20080706-5-KR-1001.01514, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1474667016403939. 17th IFAC World Congress","DOI":"10.3182\/20080706-5-KR-1001.01514"},{"key":"17_CR28","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":"17_CR29","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"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11730637_23","volume-title":"Hybrid Systems: Computation and Control","author":"Z Han","year":"2006","unstructured":"Han, Z., Krogh, B.H.: Reachability analysis of large-scale affine systems using low-dimensional polytopes. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 287\u2013301. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_23"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-99527-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2022","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: TACAS 2022. LNCS, vol. 13244, pp. 41\u201359. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3"},{"key":"17_CR32","unstructured":"Hashemi, N., Lindemann, L., Deshmukh, J.: Pca-ddreach: efficient statistical reachability analysis of stochastic dynamical systems via principal component analysis. arXiv preprint arXiv:2505.14935 (2025)"},{"key":"17_CR33","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"},{"issue":"9","key":"17_CR34","doi-asserted-by":"publisher","first-page":"4043","DOI":"10.1109\/TAC.2020.3024348","volume":"66","author":"N Kochdumper","year":"2021","unstructured":"Kochdumper, N., Althoff, M.: Sparse polynomial zonotopes: a novel set representation for reachability analysis. IEEE Trans. Autom. Control 66(9), 4043\u20134058 (2021). https:\/\/doi.org\/10.1109\/TAC.2020.3024348","journal-title":"IEEE Trans. Autom. Control"},{"key":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"2","key":"17_CR36","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C Le Guernic","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst 4(2), 250\u2013262 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 343\u2013354. IEEE (2021)","DOI":"10.1109\/ASE51524.2021.9678719"},{"key":"17_CR38","doi-asserted-by":"publisher","unstructured":"Lee, J., Yu, G., Bae, K.: SMT-based robust model checking for signal temporal logic. Sci. Comput. Program. 246, 103332 (2025). https:\/\/doi.org\/10.1016\/j.scico.2025.103332, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642325000711","DOI":"10.1016\/j.scico.2025.103332"},{"key":"17_CR39","unstructured":"Lin, A., Bansal, S.: Verification of neural reachable tubes via scenario optimization and conformal prediction. In: 6th Annual Learning for Dynamics & Control Conference, pp. 719\u2013731. PMLR (2024)"},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Lindemann, L., Qin, X., Deshmukh, J.V., Pappas, G.J.: Conformal prediction for stl runtime verification. In: Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), pp. 142\u2013153 (2023)","DOI":"10.1145\/3576841.3585927"},{"key":"17_CR41","unstructured":"Lindemann, L., Zhao, Y., Yu, X., Pappas, G.J., Deshmukh, J.V.: Formal verification and control with conformal prediction. arXiv preprint arXiv:2409.00536 (2024)"},{"key":"17_CR42","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"},{"issue":"4","key":"17_CR43","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1137\/1020098","volume":"20","author":"C Moler","year":"1978","unstructured":"Moler, C., Van Loan, C.: Nineteen dubious ways to compute the exponential of a matrix. SIAM Rev. 20(4), 801\u2013836 (1978)","journal-title":"SIAM Rev."},{"issue":"6","key":"17_CR44","doi-asserted-by":"publisher","first-page":"2700","DOI":"10.1109\/TAC.2021.3090525","volume":"67","author":"MS Mufid","year":"2022","unstructured":"Mufid, M.S., Adzkiya, D., Abate, A.: SMT-based reachability analysis of high dimensional interval max-plus linear systems. IEEE Trans. Autom. Control 67(6), 2700\u20132714 (2022). https:\/\/doi.org\/10.1109\/TAC.2021.3090525","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3","key":"17_CR45","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2168773.2168781","volume":"38","author":"J Niesen","year":"2012","unstructured":"Niesen, J., Wright, W.M.: Algorithm 919: a krylov subspace algorithm for evaluating the $$\\phi $$-functions appearing in exponential integrators. ACM Trans. Math. Softw. (TOMS) 38(3), 1\u201319 (2012)","journal-title":"ACM Trans. Math. Softw. (TOMS)"},{"key":"17_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-319-46520-3_26","volume-title":"Automated Technology for Verification and Analysis","author":"H Roehm","year":"2016","unstructured":"Roehm, H., Oehlerking, J., Heinz, T., Althoff, M.: STL model checking of continuous and hybrid systems. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 412\u2013427. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_26"},{"key":"17_CR47","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163\u2013203 (2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.06.002, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1574013710000407","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"17_CR48","unstructured":"Shafer, G., Vovk, V.: A tutorial on conformal prediction. J. Mach. Learn. Res. 9(3) (2008)"},{"key":"17_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-662-46681-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SEZ Soudjani","year":"2015","unstructured":"Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST$$^{\\sf 2}$$: Formal Abstractions of Uncountable- STate STochastic Processes. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272\u2013286. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_23"},{"key":"17_CR50","doi-asserted-by":"publisher","unstructured":"Tran, H.D., Choi, S.W., Li, Y., Liu, Q., Okamoto, H., Hoxha, B., Fainekos, G.: Starv: a qualitative and quantitative verification tool for learning-enabled systems. In: International Conference on Computer Aided Verification, pp. 376\u2013394. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_17","DOI":"10.1007\/978-3-031-98679-6_17"},{"key":"17_CR51","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S., Li, Y., Okamoto, H., Hoxha, B., Fainekos, G.: Probstar temporal logic for verifying complex behaviors of learning-enabled systems. In: Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control (2025)","DOI":"10.1145\/3716863.3718035"},{"key":"17_CR52","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S., Okamoto, H., Hoxha, B., Fainekos, G., Prokhorov, D.: Quantitative verification for neural networks using probstars. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201312 (2023)","DOI":"10.1145\/3575870.3587112"},{"key":"17_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"H-D Tran","year":"2019","unstructured":"Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39"},{"key":"17_CR54","unstructured":"Tran, H.D., Nguyen, L.V., Johnson, T.T.: Large-scale linear systems from order-reduction (benchmark proposal). In: 3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH), Vienna, Austria (2016)"},{"key":"17_CR55","unstructured":"Vovk, V., Gammerman, A., Shafer, G.: Algorithmic Learning in a Random World. Springer, Cham (2005)"},{"issue":"1","key":"17_CR56","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1137\/16M1063733","volume":"38","author":"H Wang","year":"2017","unstructured":"Wang, H., Ye, Q.: Error bounds for the Krylov subspace methods for computations of matrix exponentials. SIAM J. Matrix Anal. Appl. 38(1), 155\u2013187 (2017)","journal-title":"SIAM J. Matrix Anal. Appl."},{"key":"17_CR57","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. HSCC 2023, Association for Computing Machinery, New York (2023). https:\/\/doi.org\/10.1145\/3575870.3587121","DOI":"10.1145\/3575870.3587121"},{"key":"17_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-319-41528-4_25","volume-title":"Computer Aided Verification","author":"B Xue","year":"2016","unstructured":"Xue, B., She, Z., Easwaran, A.: Under-approximating backward reachable sets by polytopes. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 457\u2013476. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_25"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:13Z","timestamp":1762816693000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}