{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:07:50Z","timestamp":1779034070415,"version":"3.51.4"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Safe controller synthesis with formal guarantees is widely employed in safety-critical systems. However, existing controller synthesis methods are subject to significant limitations in scalability and efficiency. This paper presents a novel controller incremental synthesis framework guided by barrier certificates (BCs), thereby generating a safe controller with BC verification. To enhance verification efficiency, we construct a learning-enabled polynomial BC combined with efficient post-verification, which is transformed into smaller-scale linear Programming (LP) subproblems for feasibility determination. Furthermore, we have implemented a tool called\n                    <jats:italic>ISafeC<\/jats:italic>\n                    and evaluated its performance over a set of benchmark examples. The comparative experimental results demonstrate the effectiveness and efficiency of our approach.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_22","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:28Z","timestamp":1779033028000},"page":"419-439","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Incremental Synthesis of\u00a0Safe Controller Guided by\u00a0Learning-Enabled Barrier Certificates with\u00a0Efficient LP Verification"],"prefix":"10.1007","author":[{"given":"Niuniu","family":"Qi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanrui","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhengfeng","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xia","family":"Zeng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengxin","family":"Ren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Peng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiming","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: Fossil: a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In: Proceedings of the 24th HSCC, pp. 1\u201311 (2021)","DOI":"10.1145\/3447928.3456646"},{"key":"22_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2023.100614","volume":"51","author":"N Al-lQubaydhi","year":"2024","unstructured":"Al-lQubaydhi, N., et al.: Deep learning for unmanned aerial vehicles detection: a review. Comput. Sci. Rev. 51, 100614 (2024)","journal-title":"Comput. Sci. Rev."},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"1496","DOI":"10.1109\/LCSYS.2025.3579779","volume":"9","author":"A Alavi","year":"2025","unstructured":"Alavi, A., Nadali, A., Zamani, M., Jafarpour, S.: Neural barrier certificates for monotone systems. IEEE Control. Syst. Lett. 9, 1496\u20131501 (2025)","journal-title":"IEEE Control. Syst. Lett."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: theory and applications. In: 17th European Control Conference, ECC 2019, Naples, Italy, June 25-28, 2019, pp. 3420\u20133431 (2019). https:\/\/doi.org\/10.23919\/ECC.2019.8796030","DOI":"10.23919\/ECC.2019.8796030"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Andersen, E.D., Andersen, K.D.: The MOSEK interior point optimizer for linear programming: an implementation of the homogeneous algorithm. In: High Performance Optimization, pp. 197\u2013232. Springer (2000)","DOI":"10.1007\/978-1-4757-3216-0_8"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"582","DOI":"10.1007\/978-3-030-53288-8_29","volume-title":"Computer Aided Verification","author":"X Chen","year":"2020","unstructured":"Chen, X., Peng, C., Lin, W., Yang, Z., Zhang, Y., Li, X.: A novel approach for solving the BMI problem in barrier certificates generation. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 582\u2013603. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_29"},{"issue":"10","key":"22_CR7","doi-asserted-by":"publisher","first-page":"1846","DOI":"10.1109\/TAC.2004.835589","volume":"49","author":"G Chesi","year":"2004","unstructured":"Chesi, G.: Computing output feedback controllers to enlarge the domain of attraction in polynomial systems. IEEE Trans. Autom. Control 49(10), 1846\u20131853 (2004)","journal-title":"IEEE Trans. Autom. Control"},{"key":"22_CR8","unstructured":"Compton, W.D., Cohen, M.H., Ames, A.D.: Learning for layered safety-critical control with predictive control barrier functions. In: 7th Annual Learning for Dynamics & Control Conference, Ann Arbor, MI, USA, 4-6 June 2025. vol.\u00a0283, pp. 153\u2013165 (2025). https:\/\/proceedings.mlr.press\/v283\/compton25a.html"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Deshmukh, J.V., Kapinski, J., Yamaguchi, T., Prokhorov, D.V.: Learning deep neural network controllers for dynamical systems with safety guarantees: Invited paper. In: Proceedings of the International Conference on Computer-Aided Design, ICCAD 2019, Westminster, CO, USA, November 4-7, 2019, pp.\u00a01\u20137 (2019). https:\/\/doi.org\/10.1109\/ICCAD45719.2019.8942130","DOI":"10.1109\/ICCAD45719.2019.8942130"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Edwards, A., Peruffo, A., Abate, A.: Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models. In: International Conference on Hybrid Systems: Computation and Control, HSCC, pp. 26:1\u201326:10 (2024)","DOI":"10.1145\/3641513.3651398"},{"key":"22_CR11","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 - 18th International Symposium, ATVA. vol. 12302, pp. 537\u2013542 (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_30","DOI":"10.1007\/978-3-030-59152-6_30"},{"key":"22_CR12","unstructured":"Gao, S.: Quadcopter model (2016). https:\/\/github.com\/dreal\/benchmarks"},{"key":"22_CR13","first-page":"1437","volume":"16","author":"J Garc\u00eda","year":"2015","unstructured":"Garc\u00eda, J., Fern\u00e1ndez, F.: A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res. 16, 1437\u20131480 (2015)","journal-title":"J. Mach. Learn. Res."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Goubault, E., Mullier, O., Putot, S., Kieffer, M.: Inner approximated reachability analysis. In: 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC\u201914, Berlin, Germany, April 15-17, 2014, pp. 163\u2013172 (2014). https:\/\/doi.org\/10.1145\/2562059.2562113","DOI":"10.1145\/2562059.2562113"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017, pp. 1\u201310 (2017). https:\/\/doi.org\/10.1145\/3049797.3049811","DOI":"10.1145\/3049797.3049811"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: RINO: robust inner and outer approximated reachability of neural networks controlled systems. In: Computer Aided Verification - 34th International Conference, CAV, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. vol. 13371, pp. 511\u2013523 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_25","DOI":"10.1007\/978-3-031-13185-1_25"},{"key":"22_CR17","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2023). https:\/\/www.gurobi.com\/documentation\/"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: a polynomial arithmetic framework for verifying neural-network controlled systems. In: Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13505, pp. 414\u2013430 (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_27","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"22_CR19","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":"2","key":"22_CR20","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/s12559-023-10215-7","volume":"16","author":"F Jiang","year":"2024","unstructured":"Jiang, F., Wang, Z., Yue, G.: A novel cognitively inspired deep learning approach to detect drivable areas for self-driving cars. Cogn. Comput. 16(2), 517\u2013533 (2024)","journal-title":"Cogn. Comput."},{"key":"22_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysconle.2024.105807","volume":"188","author":"M Kamaldar","year":"2024","unstructured":"Kamaldar, M., Hoagg, J.B.: Lyapunov-like functions for almost global convergence in discrete-time systems. Syst. Control Lett. 188, 105807 (2024)","journal-title":"Syst. Control Lett."},{"issue":"6","key":"22_CR22","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/EMB.2007.907086","volume":"26","author":"R Kelley","year":"2007","unstructured":"Kelley, R.: Systems biology in practice: concepts, implementation, and application. IEEE Eng. Med. Biol. Mag. 26(6), 9\u201354 (2007)","journal-title":"IEEE Eng. Med. Biol. Mag."},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: NASA Formal Methods - 15th International Symposium, NFM, Houston, TX, USA, May 16-18, 2023, Proceedings. vol. 13903, pp. 16\u201336 (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2","DOI":"10.1007\/978-3-031-33170-1_2"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Komoda, K., et al.: Hybrid-AI grasp planning system that integrates rule-based and DNN-based methods for throughput improvement of picking robots. In: IEEE International Conference on Advanced Intelligent Mechatronics, AIM, Boston, MA, USA, July 15-19, 2024, pp. 691\u2013696 (2024). https:\/\/doi.org\/10.1109\/AIM55361.2024.10636988","DOI":"10.1109\/AIM55361.2024.10636988"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"60570","DOI":"10.1109\/ACCESS.2025.3557372","volume":"13","author":"D Kumar","year":"2025","unstructured":"Kumar, D., Raj, J., Raghuwaiya, K., Vanualailai, J.: Lyapunov-controlled quadrotor landings on dynamic mobile platforms. IEEE Access 13, 60570\u201360588 (2025)","journal-title":"IEEE Access"},{"issue":"2","key":"22_CR26","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1137\/040603942","volume":"15","author":"JB Lasserre","year":"2005","unstructured":"Lasserre, J.B.: Polynomial programming: LP-relaxations also converge. SIAM J. Optim. 15(2), 383\u2013393 (2005)","journal-title":"SIAM J. Optim."},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Lopez, D.M., Choi, S.W., Tran, H., Johnson, T.T.: NNV 2.0: the neural network verification tool. In: Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 397\u2013412 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_19","DOI":"10.1007\/978-3-031-37703-7_19"},{"key":"22_CR28","unstructured":"Papachristodoulou, A., Anderson, J., Valmorbida, G., Prajna, S., Seiler, P., Parrilo, P.A.: SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB. CoRR abs\/1310.4716 (2013). http:\/\/arxiv.org\/abs\/1310.4716"},{"key":"22_CR29","doi-asserted-by":"publisher","first-page":"117943","DOI":"10.1109\/ACCESS.2025.3584253","volume":"13","author":"OS Patil","year":"2025","unstructured":"Patil, O.S., Le, D.M., Griffis, E.J., Dixon, W.E.: Lyapunov-based deep residual neural network (ResNet) adaptive control. IEEE Access 13, 117943\u2013117952 (2025)","journal-title":"IEEE Access"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"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"},{"issue":"8","key":"22_CR31","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.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"S.\u00a0Boyd, L.V.: Convex optimization. Cambridge University Press (2004)","DOI":"10.1017\/CBO9780511804441"},{"key":"22_CR33","unstructured":"Sassi, M.A.B., Sankaranarayanan, S.: Stabilization of polynomial dynamical systems using linear programming based on Bernstein polynomials (2015)"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Saveriano, M., Lee, D.: Learning barrier functions for constrained motion planning with dynamical systems. In: 2019 IEEE\/RSJ International Conference on Intelligent Robots and Systems, IROS 2019, Macau, SAR, China, November 3-8, 2019, pp. 112\u2013119 (2019). https:\/\/doi.org\/10.1109\/IROS40897.2019.8967981","DOI":"10.1109\/IROS40897.2019.8967981"},{"key":"22_CR35","doi-asserted-by":"publisher","first-page":"2709","DOI":"10.1109\/LCSYS.2024.3511407","volume":"8","author":"M Serry","year":"2024","unstructured":"Serry, M., Liu, J.: Underapproximating safe domains of attraction for discrete-time systems using implicit representations of backward reachable sets. IEEE Control. Syst. Lett. 8, 2709\u20132714 (2024)","journal-title":"IEEE Control. Syst. Lett."},{"key":"22_CR36","doi-asserted-by":"crossref","unstructured":"Srinivasan, M., Dabholkar, A., Coogan, S., Vela, P.A.: Synthesis of control barrier functions using a supervised machine learning approach. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, IROS 2020, Las Vegas, NV, USA, October 24, 2020 - January 24, 2021, pp. 7139\u20137145 (2020). https:\/\/doi.org\/10.1109\/IROS45743.2020.9341190","DOI":"10.1109\/IROS45743.2020.9341190"},{"key":"22_CR37","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, DAC, San Francisco, CA, USA, June 24-29, 2018, pp. 30:1\u201330:6 (2018). https:\/\/doi.org\/10.1145\/3195970.3199852","DOI":"10.1109\/DAC.2018.8465843"},{"key":"22_CR38","unstructured":"Turchetta, M., Kolobov, A., Shah, S., Krause, A., Agarwal, A.: Safe reinforcement learning via curriculum induction. In: Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems (2020)"},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"Wang, Y., Chen, H., Lin, W., Ding, Z.: Formal synthesis of neural barrier certificates for dynamical systems via DC programming. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 44(10), 4038\u20134042 (2025)","DOI":"10.1109\/TCAD.2025.3555513"},{"key":"22_CR40","unstructured":"Xiang, W., Tran, H., Johnson, T.T.: Reachable set computation and safety verification for neural networks with RELU activations. CoRR abs\/1712.08163 (2017). http:\/\/arxiv.org\/abs\/1712.08163"},{"key":"22_CR41","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"},{"issue":"10","key":"22_CR42","doi-asserted-by":"publisher","first-page":"5185","DOI":"10.1109\/TAC.2017.2694351","volume":"62","author":"B Xue","year":"2017","unstructured":"Xue, B., She, Z., Easwaran, A.: Underapproximating backward reachable sets by semialgebraic sets. IEEE Trans. Autom. Control 62(10), 5185\u20135197 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"22_CR43","doi-asserted-by":"crossref","unstructured":"Yang, Z., Zhang, L., Zeng, X., Tang, X., Peng, C., Zeng, Z.: Hybrid controller synthesis for nonlinear systems subject to reach-avoid constraints. In: Computer Aided Verification - 35th International Conference, CAV, Paris, France, July 17-22, 2023, Proceedings, Part I. vol. 13964, pp. 304\u2013325 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_16","DOI":"10.1007\/978-3-031-37706-8_16"},{"key":"22_CR44","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":"22_CR45","doi-asserted-by":"publisher","DOI":"10.1016\/j.compchemeng.2024.108979","volume":"195","author":"J Yao","year":"2025","unstructured":"Yao, J., Han, M., Yin, X.: Lyapunov-based distributed reinforcement learning control with stability guarantee. Comput. Chem. Eng. 195, 108979 (2025)","journal-title":"Comput. Chem. Eng."},{"key":"22_CR46","doi-asserted-by":"crossref","unstructured":"Zeng, X., Lin, W., Yang, Z., Chen, X., Wang, L.: Darboux-type barrier certificates for safety verification of nonlinear hybrid systems. In: 2016 International Conference on Embedded Software, EMSOFT 2016, Pittsburgh, Pennsylvania, USA, October 1-7, 2016, pp. 11:1\u201311:10 (2016). https:\/\/doi.org\/10.1145\/2968478.2968484","DOI":"10.1145\/2968478.2968484"},{"key":"22_CR47","doi-asserted-by":"crossref","unstructured":"Zeng, X., Liu, B., Zeng, Z., Liu, Z., Yang, Z.: Safe controller synthesis for nonlinear systems via reinforcement learning and PAC approximation. In: Proceedings of the 61st ACM\/IEEE Design Automation Conference, DAC, San Francisco, CA, USA, June 23-27, 2024, pp. 283:1\u2013283:6 (2024). https:\/\/doi.org\/10.1145\/3649329.3657332","DOI":"10.1145\/3649329.3657332"},{"key":"22_CR48","doi-asserted-by":"crossref","unstructured":"Zeng, X., Ren, M., Liu, Z., Yang, Z.: Learning-aided safe controller synthesis with formal guarantees via vector barrier certificates. In: 62nd ACM\/IEEE Design Automation Conference, DAC, San Francisco, CA, USA, June 22-25, 2025, pp.\u00a01\u20137 (2025). https:\/\/doi.org\/10.1109\/DAC63849.2025.11132490","DOI":"10.1109\/DAC63849.2025.11132490"},{"key":"22_CR49","doi-asserted-by":"crossref","unstructured":"Zhao, H., Liu, B., Dehbi, L., Xie, H., Yang, Z., Qian, H.: Polynomial neural barrier certificate synthesis of hybrid systems via counterexample guidance. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 43(11), 3756\u20133767 (2024)","DOI":"10.1109\/TCAD.2024.3447226"},{"key":"22_CR50","doi-asserted-by":"crossref","unstructured":"Zhao, H., Qi, N., Dehbi, L., Zeng, X., Yang, Z.: Formal synthesis of neural barrier certificates for continuous systems via counterexample guided learning. ACM Trans. Embed. Comput. Syst. 22(5s), 146:1\u2013146:21 (2023)","DOI":"10.1145\/3609125"},{"key":"22_CR51","doi-asserted-by":"crossref","unstructured":"Zhao, H., Qi, N., Ren, M., Zeng, X., Zeng, Z., Yang, Z.: Neural barrier certificates synthesis of NN-controlled continuous systems via counterexample-guided learning. In: Proceedings of the 61st ACM\/IEEE Design Automation Conference, DAC. p.\u00a06 (2024). https:\/\/doi.org\/10.1145\/3649329.3658256","DOI":"10.1145\/3649329.3658256"},{"key":"22_CR52","doi-asserted-by":"crossref","unstructured":"Zhao, H., Zeng, X., Qi, N., Yang, Z., Zeng, Z.: Safe DNN-type controller synthesis for nonlinear systems via meta reinforcement learning. In: 60th ACM\/IEEE Design Automation Conference, DAC, San Francisco, CA, USA, July 9-13, 2023, pp.\u00a01\u20136 (2023). https:\/\/doi.org\/10.1109\/DAC56929.2023.10247837","DOI":"10.1109\/DAC56929.2023.10247837"},{"issue":"3","key":"22_CR53","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/s00165-021-00544-5","volume":"33","author":"H Zhao","year":"2021","unstructured":"Zhao, H., Zeng, X., Chen, T., Liu, Z., Woodcock, J.: Learning safe neural network controllers with barrier certificates. Formal Aspects Comput. 33(3), 437\u2013455 (2021). https:\/\/doi.org\/10.1007\/s00165-021-00544-5","journal-title":"Formal Aspects Comput."},{"key":"22_CR54","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: HSCC \u201922: 25th ACM International Conference on Hybrid Systems: Computation and Control, Milan, Italy, May 4 - 6, 2022, pp. 3:1\u20133:11 (2022). https:\/\/doi.org\/10.1145\/3501710.3519511","DOI":"10.1145\/3501710.3519511"},{"key":"22_CR55","doi-asserted-by":"crossref","unstructured":"Zhu, H., Xiong, Z., Magill, S., Jagannathan, S.: An inductive synthesis framework for verifiable reinforcement learning. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, Phoenix, AZ, USA, June 22-26, 2019, pp. 686\u2013701 (2019). https:\/\/doi.org\/10.1145\/3314221.3314638","DOI":"10.1145\/3314221.3314638"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:34Z","timestamp":1779033034000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}