{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:04:51Z","timestamp":1770750291424,"version":"3.50.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"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-11176-0_9","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:21Z","timestamp":1763842281000},"page":"124-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Iteratively Synthesizing $$\\epsilon $$-Robust Barrier Certificates for\u00a0Neural Network Controlled Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-3182-183X","authenticated-orcid":false,"given":"Yi","family":"Luo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0613-7158","authenticated-orcid":false,"given":"Xin","family":"Chen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4121-4114","authenticated-orcid":false,"given":"Jin","family":"Dai","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9004-1292","authenticated-orcid":false,"given":"Enyi","family":"Tang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3090-9568","authenticated-orcid":false,"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"9_CR1","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":"9_CR2","doi-asserted-by":"publisher","unstructured":"Bacci, E., Parker, D.: Verified probabilistic policies for deep reinforcement learning. In: Proceedings of 14th International Symposium on NASA Formal Methods. Lecture Notes in Computer Science, vol. 13260, pp. 193\u2013212. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_10","DOI":"10.1007\/978-3-031-06773-0_10"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1613\/jair.1.12963","volume":"72","author":"S Carr","year":"2021","unstructured":"Carr, S., Jansen, N., Topcu, U.: Task-aware verifiable rnn-based policies for partially observable markov decision processes. J. Artif. Intell. Res. 72, 819\u2013847 (2021)","journal-title":"J. Artif. Intell. Res."},{"issue":"3","key":"9_CR4","doi-asserted-by":"publisher","first-page":"1749","DOI":"10.1109\/TRO.2022.3232542","volume":"39","author":"C Dawson","year":"2023","unstructured":"Dawson, C., Gao, S., Fan, C.: Safe control with learned certificates: a survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Trans. Rob. 39(3), 1749\u20131767 (2023)","journal-title":"IEEE Trans. Rob."},{"key":"9_CR5","unstructured":"Dean, S., Taylor, A.J., Cosner, R.K., Recht, B., Ames, A.D.: Guaranteeing safety of learned perception modules via measurement-robust control barrier functions. In: Proceedings of 4th Conference on Robot Learning, CoRL 2020. Proceedings of Machine Learning Research, vol.\u00a0155, pp. 654\u2013670. PMLR (2020)"},{"key":"9_CR6","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. CoRR arxiv:1810.12715 (2018)"},{"issue":"5s","key":"9_CR7","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. (TECS) 18(5s), 1\u201322 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"9_CR8","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":"9_CR9","first-page":"1","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. (TECS) 20(1), 1\u201326 (2020)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"9_CR10","unstructured":"Julian, K.D., Kochenderfer, M.J.: A reachability method for verifying dynamical systems with deep neural network controllers (2019)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-39799-8_17","volume-title":"Computer Aided Verification","author":"H Kong","year":"2013","unstructured":"Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242\u2013257. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_17"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Mitra, S., et al.: Formal verification techniques for vision-based autonomous systems \u2013 a survey, pp. 89\u2013108. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_5","DOI":"10.1007\/978-3-031-75778-5_5"},{"issue":"8","key":"9_CR14","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131429 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Sha, M., et al.: Synthesizing barrier certificates of neural network controlled continuous systems via approximations. In: Proceedings of 58th ACM\/IEEE Design Automation Conference, pp. 631\u2013636 (2021)","DOI":"10.1109\/DAC18074.2021.9586327"},{"key":"9_CR16","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems, pp. 10802\u201310813 (2018)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Sun, S., Zhang, Y., Luo, X., Vlantis, P., Pajic, M., Zavlanos, M.M.: Formal verification of stochastic systems with relu neural network controllers. In: Proceedings of 2022 International Conference on Robotics and Automation, ICRA 2022, pp. 6800\u20136806. IEEE (2022)","DOI":"10.1109\/ICRA46639.2022.9811866"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 147\u2013156 (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Tuncali, C.E., Kapinski, J., Ito, H., Deshmukh, J.V.: Reasoning about safety of learning-enabled components in autonomous cyber-physical systems. In: Proceedings of the 55th Annual Design Automation Conference, pp.\u00a01\u20136 (2018)","DOI":"10.1145\/3195970.3199852"},{"key":"9_CR20","unstructured":"Waite, T., Robey, A., Hassani, H., Pappas, G.J., Ivanov, R.: Data-driven modeling and verification of perception-based autonomous systems. CoRR arxiv:2312.06848 (2023)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Wang, Y., Zarei, M., Bonakdarpour, B., Pajic, M.: Statistical verification of hyperproperties for cyber-physical systems. ACM Trans. Embed. Comput. Syst. 18(5s), 92:1\u201392:23 (2019)","DOI":"10.1145\/3358232"},{"key":"9_CR22","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. In: Proceedings of 33th Annual Conference on Neural Information Processing Systems, NeurIPS 2020 (2020)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-030-81685-8_22","volume-title":"Computer Aided Verification","author":"Z Yang","year":"2021","unstructured":"Yang, Z., et al.: An iterative scheme of safe reinforcement learning for nonlinear systems via barrier certificate generation. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 467\u2013490. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_22"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Zarei, M., Wang, Y., Pajic, M.: Statistical verification of learning-based cyber-physical systems. In: Proceedings of 23rd ACM International Conference on Hybrid Systems: Computation and Control, pp. 12:1\u201312:7. ACM (2020)","DOI":"10.1145\/3365365.3382209"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Zeng, X., Yang, Z., Zhang, L., Tang, X., Zeng, Z., Liu, Z.: Safety verification of nonlinear systems with bayesian neural network controllers. In: Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, pp. 15278\u201315286. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i12.26782"},{"issue":"1","key":"9_CR26","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/s12083-022-01434-0","volume":"16","author":"H Zhang","year":"2023","unstructured":"Zhang, H., et al.: Backdoor attacks against deep reinforcement learning based traffic signal control systems. Peer Peer Netw. Appl. 16(1), 466\u2013474 (2023)","journal-title":"Peer Peer Netw. Appl."},{"key":"9_CR27","unstructured":"Zhang, H., et al.: Robust deep reinforcement learning against adversarial perturbations on state observations. In: Proceedings of 33th Annual Conference on Neural Information Processing Systems (2020)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Zhao, Q., Chen, X., Zhao, Z., Zhang, Y., Tang, E., Li, X.: Verifying neural network controlled systems using neural networks. In: Proceedings of 25th ACM International Conference on Hybrid Systems: Computation and Control, pp. 3:1\u20133:11. ACM (2022)","DOI":"10.1145\/3501710.3519511"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Zhi, D., Wang, P., Liu, S., Ong, C.L., Zhang, M.: Unifying qualitative and quantitative safety verification of dnn-controlled systems. In: Proceedings of 36th International Conference on Computer Aided Verification, CAV 2024. Lecture Notes in Computer Science, vol. 14682, pp. 401\u2013426. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_20","DOI":"10.1007\/978-3-031-65630-9_20"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:14Z","timestamp":1770721754000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","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":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}