{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T22:41:20Z","timestamp":1784328080964,"version":"3.55.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031606977","type":"print"},{"value":"9783031606984","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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-60698-4_14","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"239-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Compositional Inductive Invariant Based Verification of\u00a0Neural Network Controlled Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6895-6308","authenticated-orcid":false,"given":"Yuhao","family":"Zhou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1777-493X","authenticated-orcid":false,"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/s10458-021-09529-3","volume":"36","author":"ME Akintunde","year":"2022","unstructured":"Akintunde, M.E., Botoeva, E., Kouvaros, P., Lomuscio, A.: Formal verification of neural agents in non-deterministic environments. Auton. Agents Multi-Agent Syst. 36, 6 (2022)","journal-title":"Auton. Agents Multi-Agent Syst."},{"key":"14_CR2","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)"},{"key":"14_CR3","unstructured":"Amir, G., Schapira, M., Katz, G.: Towards scalable verification of deep reinforcement learning. In: Formal Methods in Computer Aided Design (FMCAD) (2021)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: Proceedings of the International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization (2021)","DOI":"10.24963\/ijcai.2021\/297"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bak, S.: nnenum: verification of ReLU neural networks with optimized abstraction refinement. In: NASA Formal Methods Symposium (2021)","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (2019)","DOI":"10.1145\/3302504.3311804"},{"key":"14_CR7","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":"14_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Deshmukh, J.V., Kapinski, J.P., Yamaguchi, T., Prokhorov, D.: Learning deep neural network controllers for dynamical systems with safety guarantees. In: 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). IEEE (2019)","DOI":"10.1109\/ICCAD45719.2019.8942130"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-030-25540-4_25","volume-title":"Computer Aided Verification (CAV)","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, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_25"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Jha, S., Sankaranarayanan, S., Tiwari, A.: Sherlock-a tool for verification of neural network feedback systems: demo abstract. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (2019)","DOI":"10.1145\/3302504.3313351"},{"key":"14_CR13","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI (2018)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Eleftheriadis, C., Kekatos, N., Katsaros, P., Tripakis, S.: On neural network equivalence checking using SMT solvers. In: 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022) (2022)","DOI":"10.1007\/978-3-031-15839-1_14"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Eliyahu, T., Kazak, Y., Katz, G., Schapira, M.: Verifying learning-augmented systems. In: Proceedings of the 2021 ACM SIGCOMM 2021 Conference (2021)","DOI":"10.1145\/3452296.3472936"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Fan, J., Huang, C., Chen, X., Li, W., Zhu, Q.: ReachNN*: a tool for reachability analysis of neural-network controlled systems. In: Automated Technology for Verification and Analysis (2020)","DOI":"10.1007\/978-3-030-59152-6_30"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP) (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.: On symmetry and quantification: a new approach to verify distributed protocols. In: NASA Formal Methods Symposium (2021)","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-59152-6_4","volume-title":"ATVA 2020","author":"M Goyal","year":"2020","unstructured":"Goyal, M., Duggirala, P.S.: Neuralexplorer: state space exploration of closed loop control systems using neural networks. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 75\u201391. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_4"},{"key":"14_CR20","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., Holik, L., Wu, Z. (eds.) ATVA 2022, pp. 414\u2013430. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_27","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"14_CR21","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. (TECS) (2019)","DOI":"10.1145\/3358228"},{"key":"14_CR22","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., Kuncak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"14_CR23","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, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_11"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (2019)","DOI":"10.1145\/3302504.3311806"},{"key":"14_CR25","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., Kuncak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"14_CR26","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"CAV 2019","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"14_CR27","unstructured":"Lopez, D.M., Althoff, M., Forets, M., Johnson, T.T., Ladner, T., Schilling, C.: ARCH-COMP23 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23). EPiC Series in Computing (2023)"},{"key":"14_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Kasiviswanathan, S., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"14_CR30","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/2914770.2837640","volume":"51","author":"O Padon","year":"2016","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. ACM SIGPLAN Not. 51, 217\u2013231 (2016)","journal-title":"ACM SIGPLAN Not."},{"key":"14_CR31","unstructured":"Paszke, A., et\u00a0al.: Pytorch: an imperative style, high-performance deep learning library. In: Advances in Neural Information Processing Systems (2019)"},{"key":"14_CR32","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"International Workshop on 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"},{"key":"14_CR33","first-page":"1","volume":"22","author":"A Raffin","year":"2021","unstructured":"Raffin, A., Hill, A., Gleave, A., Kanervisto, A., Ernestus, M., Dormann, N.: Stable-baselines3: reliable reinforcement learning implementations. J. Mach. Learn. Res. 22, 1\u20138 (2021)","journal-title":"J. Mach. Learn. Res."},{"key":"14_CR34","unstructured":"Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: CLN2INV: learning loop invariants with continuous logic networks. arXiv preprint arXiv:1909.11542 (2019)"},{"key":"14_CR35","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 (2022)","DOI":"10.1609\/aaai.v36i7.20790"},{"key":"14_CR36","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Plain and simple inductive invariant inference for distributed protocols in TLA+. In: Formal Methods in Computer-Aided Design (FMCAD) (2022)"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Sha, M., et al.: Synthesizing barrier certificates of neural network controlled continuous systems via approximations. In: ACM\/IEEE Design Automation Conference. IEEE (2021)","DOI":"10.1109\/DAC18074.2021.9586327"},{"key":"14_CR38","first-page":"1","volume":"31","author":"G Singh","year":"2018","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. Adv. Neural Inf. Process. Syst. 31, 1\u201312 (2018)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"14_CR39","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-319-95582-7_25","volume-title":"International Symposium on Formal Methods","author":"A Sogokon","year":"2018","unstructured":"Sogokon, A., Ghorbal, K., Tan, Y.K., Platzer, A.: Vector barrier certificates and comparison systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 418\u2013437. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_25"},{"key":"14_CR40","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: ICLR (2019)"},{"key":"14_CR41","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"International Conference on Computer Aided Verification","author":"HD 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., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"14_CR42","doi-asserted-by":"crossref","unstructured":"Viswanadha, K., Kim, E., Indaheng, F., Fremont, D.J., Seshia, S.A.: Parallel and multi-objective falsification with scenic and verifai. In: Runtime Verification: 21st International Conference (2021)","DOI":"10.1007\/978-3-030-88494-9_15"},{"key":"14_CR43","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-81685-8_21","volume-title":"International Conference on Computer Aided Verification","author":"Q Wang","year":"2021","unstructured":"Wang, Q., Chen, M., Xue, B., Zhan, N., Katoen, J.P.: Synthesizing invariant barrier certificates via difference-of-convex programming. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 443\u2013466. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_21"},{"key":"14_CR44","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security 2018). USENIX Association (2018)"},{"key":"14_CR45","first-page":"29909","volume":"34","author":"S Wang","year":"2021","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. Adv. Neural Inf. Process. Syst. 34, 29909\u201329921 (2021)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"14_CR46","first-page":"1129","volume":"33","author":"K Xu","year":"2020","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. Adv. Neural Inf. Process. Syst. 33, 1129\u20131141 (2020)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"14_CR47","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2020.106296","volume":"123","author":"J Zhang","year":"2020","unstructured":"Zhang, J., Li, J.: Testing and verification of neural-network-based safety-critical control software: a systematic literature review. Inf. Softw. Technol. 123, 106296 (2020)","journal-title":"Inf. Softw. Technol."},{"key":"14_CR48","unstructured":"Zhou, Y., Tripakis, S.: Compositional inductive invariant based verification of neural network controlled systems. arXiv eprint arxiv:2312.10842 (2023)"}],"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-60698-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:03:56Z","timestamp":1716768236000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","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":"Moffett Field, 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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}