{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:47:25Z","timestamp":1778122045345,"version":"3.51.4"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031505201","type":"print"},{"value":"9783031505218","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-50521-8_4","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T08:03:15Z","timestamp":1703836995000},"page":"73-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Taming Reachability Analysis of\u00a0DNN-Controlled Systems via\u00a0Abstraction-Based Training"],"prefix":"10.1007","author":[{"given":"Jiaxu","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dapeng","family":"Zhi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Si","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peixin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"4_CR1","unstructured":"Abadi, M., et al.: Tensorflow: a system for large-scale machine learning. In: OSDI, vol. 16, pp. 265\u2013283. Savannah, GA, USA (2016)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Abel, D.: A theory of state abstraction for reinforcement learning. In: AAAI, vol. 33, pp. 9876\u20139877 (2019)","DOI":"10.1609\/aaai.v33i01.33019876"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Afzal, M., et al.: Veriabs: verification by abstraction and test generation. In: ASE, pp. 1138\u20131141. IEEE (2019)","DOI":"10.1109\/ASE.2019.00121"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Akrour, R., Veiga, F., Peters, J., Neumann, G.: Regularizing reinforcement learning with state abstraction. In: IROS, pp. 534\u2013539. IEEE (2018)","DOI":"10.1109\/IROS.2018.8594201"},{"key":"4_CR5","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Cyber-Physical Systems Virtual Organization (CPS-VO 2015), pp. 120\u2013151 (2015)"},{"issue":"2","key":"4_CR6","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1109\/TIV.2016.2622920","volume":"1","author":"M Althoff","year":"2016","unstructured":"Althoff, M., Magdici, S.: Set-based prediction of traffic participants on arbitrary road networks. IEEE Trans. Intell. Veh. 1(2), 187\u2013202 (2016)","journal-title":"IEEE Trans. Intell. Veh."},{"issue":"1","key":"4_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., et al.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-57628-8_14","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"E Bacci","year":"2020","unstructured":"Bacci, E., Parker, D.: Probabilistic guarantees for safe deep reinforcement learning. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 231\u2013248. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57628-8_14"},{"key":"4_CR9","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":"4_CR10","doi-asserted-by":"crossref","unstructured":"Baluta, T., Chua, Z.L., Meel, K.S., Saxena, P.: Scalable quantitative verification for deep neural networks. In: ICSE, pp. 312\u2013323. IEEE (2021)","DOI":"10.1109\/ICSE43902.2021.00039"},{"issue":"2","key":"4_CR11","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0005-1098(71)90066-5","volume":"7","author":"DP Bertsekas","year":"1971","unstructured":"Bertsekas, D.P., Rhodes, I.B.: On the minimax reachability of target sets and target tubes. Automatica 7(2), 233\u2013247 (1971)","journal-title":"Automatica"},{"key":"4_CR12","doi-asserted-by":"publisher","DOI":"10.1016\/j.asoc.2020.106275","volume":"92","author":"PV Campos Souza","year":"2020","unstructured":"Campos Souza, P.V.: Fuzzy neural networks and neuro-fuzzy networks: a review the main techniques and applications used in the literature. Appl. Soft Comput. 92, 106275 (2020)","journal-title":"Appl. Soft Comput."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: RTSS, pp. 183\u2013192. IEEE (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"4_CR14","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":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-030-81685-8_9","volume-title":"Computer Aided Verification","author":"M Christakis","year":"2021","unstructured":"Christakis, M., et al.: Automated safety verification of programs invoking neural networks. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 201\u2013224. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_9"},{"issue":"9","key":"4_CR16","doi-asserted-by":"publisher","first-page":"284","DOI":"10.3182\/20120606-3-NL-3011.00063","volume":"45","author":"P Collins","year":"2012","unstructured":"Collins, P., Bresolin, D., et al.: Computing the evolution of hybrid systems using rigorous function calculus. IFAC Proc. Vol. 45(9), 284\u2013290 (2012)","journal-title":"IFAC Proc. Vol."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Dong, Y., Zhao, X., Huang, X.: Dependability analysis of deep reinforcement learning based robotics and autonomous systems through probabilistic model checking. In: IROS, pp. 5171\u20135178. IEEE (2022)","DOI":"10.1109\/IROS47612.2022.9981794"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-030-25540-4_25","volume-title":"Computer Aided Verification","author":"T Dreossi","year":"2019","unstructured":"Dreossi, T., et al.: VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 432\u2013442. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_25"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Drews, S., Albarghouthi, A., D\u2019Antoni, L.: Proving data-poisoning robustness in decision trees. In: PLDI, pp. 1083\u20131097 (2020)","DOI":"10.1145\/3385412.3385975"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: HSCC, pp. 157\u2013168 (2019)","DOI":"10.1145\/3302504.3311807"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-319-63387-9_22","volume-title":"Computer Aided Verification","author":"C Fan","year":"2017","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M.: DryVR: data-driven verification and compositional reasoning for automotive systems. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 441\u2013461. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_22"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-030-59152-6_30","volume-title":"Automated Technology for Verification and Analysis","author":"J Fan","year":"2020","unstructured":"Fan, J., Huang, C., Chen, X., Li, W., Zhu, Q.: ReachNN*: a tool for reachability analysis of neural-network controlled systems. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 537\u2013542. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_30"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Fang, X., Calinescu, R., Gerasimou, S., Alhwikem, F.: Fast parametric model checking through model fragmentation. In: ICSE, pp. 835\u2013846. IEEE (2021)","DOI":"10.1109\/ICSE43902.2021.00081"},{"key":"4_CR25","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.: 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":"4_CR26","unstructured":"Gallestey, E., Hokayem, P.: Lecture notes in nonlinear systems and control (2019)"},{"issue":"5","key":"4_CR27","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/MSPEC.2016.7459105","volume":"53","author":"L Gomes","year":"2016","unstructured":"Gomes, L.: When will Google\u2019s self-driving car really be ready? It depends on where you live and what you mean by \u201cready\u2019\u2019 [news]. IEEE Spectr. 53(5), 13\u201314 (2016)","journal-title":"IEEE Spectr."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Heo, K., Oh, H., Yang, H.: Resource-aware program analysis via online abstraction coarsening. In: ICSE, pp. 94\u2013104. IEEE (2019)","DOI":"10.1109\/ICSE.2019.00027"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Hildebrandt, C., Elbaum, S., Bezzo, N.: Blending kinematic and software models for tighter reachability analysis. In: ICSE(NIER), pp. 33\u201336 (2020)","DOI":"10.1145\/3377816.3381730"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: a polynomial arithmetic framework for verifying neural-network controlled systems. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis. ATVA 2022. LNCS, vol. 13505, pp. 414\u2013430. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_27","DOI":"10.1007\/978-3-031-19992-9_27"},{"issue":"5s","key":"4_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: ReachNN: reachability analysis of neural-network controlled systems. ACM Trans. Embed. Comput. Syst. 18(5s), 1\u201322 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-81685-8_11","volume-title":"Computer Aided Verification","author":"R Ivanov","year":"2021","unstructured":"Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G., Lee, I.: Verisig 2.0: verification of neural network controllers using Taylor model preconditioning. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 249\u2013262. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_11"},{"issue":"1","key":"4_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3419742","volume":"20","author":"R Ivanov","year":"2020","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), 1\u201326 (2020)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Jin, P., Tian, J., Zhi, D., Wen, X., Zhang, M.: TRAINIFY: A CEGAR-driven training and verification framework for safe deep reinforcement learning. In: Shoham, S., Vizel, Y. (eds) Computer Aided Verification. CAV 2022. Lecture Notes in Computer Science, vol. 13371, pp. 193\u2013218. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_10","DOI":"10.1007\/978-3-031-13185-1_10"},{"issue":"7553","key":"4_CR35","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1038\/nature14539","volume":"521","author":"Y LeCun","year":"2015","unstructured":"LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436\u2013444 (2015)","journal-title":"Nature"},{"key":"4_CR36","unstructured":"Lillicrap, T.P., Hunt, J.J., Pritzel, A., et al.: Continuous control with deep reinforcement learning. In: ICLR, OpenReview.net (2016)"},{"issue":"3","key":"4_CR37","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1049\/ip-cta:20040480","volume":"152","author":"D Limon","year":"2005","unstructured":"Limon, D., Bravo, J., Alamo, T., Camacho, E.: Robust MPC of constrained nonlinear systems based on interval arithmetic. IEE Proc. Control Theory App. 152(3), 325\u2013332 (2005)","journal-title":"IEE Proc. Control Theory App."},{"issue":"3","key":"4_CR38","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"},{"key":"4_CR39","first-page":"239","volume":"6","author":"K Makino","year":"2003","unstructured":"Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math. 6, 239\u2013316 (2003)","journal-title":"Int. J. Pure Appl. Math."},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Meiss, J.D.: Differential dynamical systems, Mathematical modeling and computation, vol. 14. SIAM (2007)","DOI":"10.1137\/1.9780898718232"},{"key":"4_CR41","unstructured":"Minsky, M.L.: Computation. Prentice-Hall Englewood Cliffs, Hoboken (1967)"},{"issue":"7540","key":"4_CR42","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., Kavukcuoglu, K., Silver, D., et al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529\u2013533 (2015)","journal-title":"Nature"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to interval analysis. SIAM (2009)","DOI":"10.1137\/1.9780898717716"},{"key":"4_CR44","unstructured":"Park, S., Kim, J., Kim, G.: Time discretization-invariant safe action repetition for policy gradient methods. In: NeurIPS 2021, vol. 34, pp. 267\u2013279 (2021)"},{"key":"4_CR45","unstructured":"Paszke, A., et al.: Pytorch: an imperative style, high-performance deep learning library. In: NeurIPS, vol. 32 (2019)"},{"issue":"2","key":"4_CR46","doi-asserted-by":"publisher","first-page":"818","DOI":"10.1109\/TASE.2017.2707129","volume":"15","author":"A Pereira","year":"2017","unstructured":"Pereira, A., Althoff, M.: Over approximative human arm occupancy prediction for collision avoidance. IEEE Trans. Autom. Sci. Eng. 15(2), 818\u2013831 (2017)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Schilling, C., Forets, M., Guadalupe, S.: Verification of neural-network control systems by integrating Taylor models and zonotopes. In: AAAI, vol. 36, pp. 8169\u20138177 (2022)","DOI":"10.1609\/aaai.v36i7.20790"},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"Schmidt, L., Kontes, G., Plinge, A., Mutschler, C.: Can you trust your autonomous car? Interpretable and verifiably safe reinforcement learning. In: IV, pp. 171\u2013178. IEEE (2021)","DOI":"10.1109\/IV48863.2021.9575328"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, B., Kochdumper, N., Althoff, M.: Reached model predictive control for disturbed nonlinear systems. In: CDC, pp. 3463\u20133470. IEEE (2018)","DOI":"10.1109\/CDC.2018.8619781"},{"key":"4_CR50","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/j.automatica.2016.02.036","volume":"69","author":"J Scott","year":"2016","unstructured":"Scott, J., Raimondo, D., Marseglia, G., Braatz, R.: Constrained zonotopes: a new tool for set-based estimation and fault detection. Automatica 69, 126\u2013136 (2016)","journal-title":"Automatica"},{"key":"4_CR51","first-page":"361","volume":"7","author":"SP Singh","year":"1995","unstructured":"Singh, S.P., Jaakkola, T., Jordan, M.I.: Reinforcement learning with soft state aggregation. NeurIPS 7, 361\u2013368 (1995)","journal-title":"NeurIPS"},{"key":"4_CR52","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.asoc.2019.01.013","volume":"77","author":"M Song","year":"2019","unstructured":"Song, M., Jing, Y., Pedrycz, W.: Granular neural networks: a study of optimizing allocation of information granularity in input space. Appl. Soft Comput. 77, 67\u201375 (2019)","journal-title":"Appl. Soft Comput."},{"issue":"4","key":"4_CR53","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1109\/TSMC.2017.2710132","volume":"49","author":"J Su","year":"2017","unstructured":"Su, J., Chen, W.H.: Model-based fault diagnosis system verification using reachability analysis. IEEE Trans. Syst. Man Cybern. Syst. 49(4), 742\u2013751 (2017)","journal-title":"IEEE Trans. Syst. Man Cybern. Syst."},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: HSCC, pp. 147\u2013156 (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"4_CR55","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR (2014)"},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Tian, J., Zhi, D., Liu, S., Wang, P., Katz, G., Zhang, M.: Taming reachability analysis of DNN-controlled systems via abstraction-based training (2023)","DOI":"10.1007\/978-3-031-50521-8_4"},{"key":"4_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-030-53288-8_2","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using imagestars. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 18\u201342. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2"},{"key":"4_CR58","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., Yang, X., Manzanas Lopez, D., Musau, P., Nguyen, L.V., Xiang, W., Bak, S., Johnson, T.T.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"Wang, Z., Albarghouthi, A., Prakriya, G., Jha, S.: Interval universal approximation for neural networks. In: POPL, vol. 6, pp. 1\u201329. ACM (2022)","DOI":"10.1145\/3498675"},{"issue":"11","key":"4_CR60","doi-asserted-by":"publisher","first-page":"3944","DOI":"10.1109\/TCAD.2020.3012251","volume":"39","author":"B Xue","year":"2020","unstructured":"Xue, B., Zhang, M., Easwaran, A., Li, Q.: Pac model checking of black-box continuous-time dynamical systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11), 3944\u20133955 (2020)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"4_CR61","doi-asserted-by":"crossref","unstructured":"Zhang, Y., et al.: QVIP: an ILP-based formal verification approach for quantized neural networks. In: ASE, pp. 1\u201313. No. 80 (2022)","DOI":"10.1145\/3551349.3556916"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-50521-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:07:41Z","timestamp":1704240461000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50521-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505201","9783031505218"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50521-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","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":"74","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":"30","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":"0","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":"41% - 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","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}