{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:46:04Z","timestamp":1766043964115,"version":"3.48.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032054340"},{"type":"electronic","value":"9783032054357"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"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-05435-7_4","type":"book-chapter","created":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T01:30:34Z","timestamp":1757727034000},"page":"54-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of\u00a0Neural Certificates Done Dynamically"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8974-2542","authenticated-orcid":false,"given":"Konstantin","family":"Kueffner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4993-773X","authenticated-orcid":false,"given":"Emily","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"key":"4_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 International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2021)","DOI":"10.1145\/3447928.3456646"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Abiodun, O.I., Jantan, A., Omolara, A.E., Dada, K.V., Mohamed, N.A., Arshad, H.: State-of-the-art in artificial neural network applications: a survey. Heliyon 4(11) (2018)","DOI":"10.1016\/j.heliyon.2018.e00938"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ames, A.D., Grizzle, J.W., Tabuada, P.: Control barrier function based quadratic programs with application to adaptive cruise control. In: 53rd IEEE Conference on Decision and Control, pp. 6271\u20136278. IEEE (2014)","DOI":"10.1109\/CDC.2014.7040372"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10916-018-1088-1","volume":"42","author":"SM Anwar","year":"2018","unstructured":"Anwar, S.M., Majid, M., Qayyum, A., Awais, M., Alnowami, M., Khan, M.K.: Medical image analysis using convolutional neural networks: a review. J. Med. Syst. 42, 1\u201313 (2018)","journal-title":"J. Med. Syst."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 533\u2013548. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"4_CR6","unstructured":"Chang, Y.C., Roohi, N., Gao, S.: Neural Lyapunov control. Adv. Neural Inf. Process. Syst. 32 (2019)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Lechner, M., Zikelic, D.: A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: TACAS (1). LNCS, vol. 13993, pp. 3\u201325. Springer (2023)","DOI":"10.1007\/978-3-031-30823-9_1"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Crenshaw, T.L., Gunter, E., Robinson, C.L., Sha, L., Kumar, P.: The simplex reference model: limiting fault-propagation due to unreliable components in cyber-physical system architectures. In: 28th IEEE International Real-Time Systems Symposium (RTSS 2007), pp. 400\u2013412. IEEE (2007)","DOI":"10.1109\/RTSS.2007.34"},{"issue":"3","key":"4_CR9","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. Robot. 39(3), 1749\u20131767 (2023)","journal-title":"IEEE Trans. Robot."},{"key":"4_CR10","unstructured":"Dawson, C., Qin, Z., Gao, S., Fan, C.: Safe nonlinear control using robust neural Lyapunov-barrier functions. In: Conference on Robot Learning, pp. 1724\u20131735. PMLR (2022)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Desai, A., Ghosh, S., Seshia, S.A., Shankar, N., Tiwari, A.: SOTER: a runtime assurance framework for programming safe robotics systems. In: 2019 49th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 138\u2013150. IEEE (2019)","DOI":"10.1109\/DSN.2019.00027"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Pal, A., Tautschnig, M.: Neural model checking. In: The Thirty-eighth Annual Conference on Neural Information Processing Systems (2024)","DOI":"10.52202\/079017-2742"},{"key":"4_CR13","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024). https:\/\/www.gurobi.com"},{"key":"4_CR14","unstructured":"Henzinger, T.A., Kresse, F., Mallik, K., Yu, E., Zikelic, D.: Predictive monitoring of black-box dynamical systems. In: L4DC. Proceedings of Machine Learning Research, PMLR (2025)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Jewison, C., Erwin, R.S.: A spacecraft benchmark problem for hybrid control and estimation. In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 3300\u20133305. IEEE (2016)","DOI":"10.1109\/CDC.2016.7798765"},{"issue":"6","key":"4_CR16","doi-asserted-by":"publisher","first-page":"2042","DOI":"10.1109\/TNNLS.2017.2773458","volume":"29","author":"B Kiumarsi","year":"2017","unstructured":"Kiumarsi, B., Vamvoudakis, K.G., Modares, H., Lewis, F.L.: Optimal and autonomous control using reinforcement learning: a survey. IEEE Trans. Neural Netw. Learn. Syst. 29(6), 2042\u20132062 (2017)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Maderbacher, B., Schupp, S., Bartocci, E., Bloem, R., Ni\u010dkovi\u0107, D., K\u00f6nighofer, B.: Provable correct and adaptive simplex architecture for bounded-liveness properties. In: International Symposium on Model Checking Software, pp. 141\u2013160. Springer (2023)","DOI":"10.1007\/978-3-031-32157-3_8"},{"key":"4_CR18","unstructured":"Mandal, U., et\u00a0al.: Formally verifying deep reinforcement learning controllers with Lyapunov barrier certificates. In: # PLACEHOLDER_PARENT_METADATA_VALUE#, pp. 95\u2013106. TU Wien Academic Press (2024)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Mehmood, U., Sheikhi, S., Bak, S., Smolka, S.A., Stoller, S.D.: The black-box simplex architecture for runtime assurance of autonomous CPS. In: NASA Formal Methods Symposium, pp. 231\u2013250. Springer (2022)","DOI":"10.1007\/978-3-031-06773-0_12"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 370\u2013388. Springer (2021)","DOI":"10.1007\/978-3-030-72016-2_20"},{"issue":"1","key":"4_CR21","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/s10703-016-0265-4","volume":"51","author":"D Phan","year":"2017","unstructured":"Phan, D., Yang, J., Grosu, R., Smolka, S.A., Stoller, S.D.: Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles. Formal Methods Syst. Des. 51(1), 62\u201386 (2017). https:\/\/doi.org\/10.1007\/s10703-016-0265-4","journal-title":"Formal Methods Syst. Des."},{"issue":"8","key":"4_CR22","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":"4_CR23","doi-asserted-by":"crossref","unstructured":"Schierman, J.D., et al.: Runtime assurance framework development for highly adaptive flight control systems, Technical report, Barron Associates Inc., Charlottesville (2015)","DOI":"10.21236\/AD1010277"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Sen, K.: Concolic testing. In: Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering, pp. 571\u2013572 (2007)","DOI":"10.1145\/1321631.1321746"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Sen, K.: DART: directed automated random testing. In: Haifa Verification Conference. LNCS, vol.\u00a06405, p.\u00a04. Springer (2009)","DOI":"10.1007\/978-3-642-19237-1_4"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC\/SIGSOFT FSE, pp. 263\u2013272. ACM (2005)","DOI":"10.1145\/1095430.1081750"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Seto, D., Krogh, B., Sha, L., Chutinan, A.: The simplex architecture for safe online control system upgrades. In: Proceedings of the 1998 American Control Conference. ACC (IEEE Cat. No. 98CH36207), vol.\u00a06, pp. 3504\u20133508. IEEE (1998)","DOI":"10.1109\/ACC.1998.703255"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Smith, M.C.: The general problem of the stability of motion : translated and edited by A. T. Fuller. Taylor and Francis (1992). Automatica 31(2), 353\u2013354 (1995)","DOI":"10.1016\/0005-1098(95)90022-5"},{"key":"4_CR29","unstructured":"Sun, D., Jha, S., Fan, C.: Learning certified control using contraction metric. In: Conference on Robot Learning, pp. 1519\u20131539. PMLR (2021)"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Tayal, M., Zhang, H., Jagtap, P., Clark, A., Kolathaya, S.: Learning a formally verified control barrier function in stochastic environment. arXiv preprint arXiv:2403.19332 (2024)","DOI":"10.1109\/CDC56724.2024.10886052"},{"issue":"11","key":"4_CR31","doi-asserted-by":"publisher","first-page":"7106","DOI":"10.1109\/LRA.2023.3315211","volume":"8","author":"J Yin","year":"2023","unstructured":"Yin, J., Dawson, C., Fan, C., Tsiotras, P.: Shield model predictive path integral: a computationally efficient robust MPC method using control barrier functions. IEEE Robot. Autom. Lett. 8(11), 7106\u20137113 (2023)","journal-title":"IEEE Robot. Autom. Lett."},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Yu, E., \u017dikeli\u0107, \u0110., Henzinger, T.A.: Neural control and certificate repair via runtime monitoring. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a039, pp. 26409\u201326417 (2025)","DOI":"10.1609\/aaai.v39i25.34840"},{"key":"4_CR33","unstructured":"Zhang, H., Qin, Z., Gao, S., Clark, A.: SEEV: synthesis with efficient exact verification for Relu neural barrier functions. In: NeurIPS (2024)"},{"key":"4_CR34","first-page":"5685","volume":"36","author":"H Zhang","year":"2023","unstructured":"Zhang, H., Wu, J., Vorobeychik, Y., Clark, A.: Exact verification of Relu neural control barrier functions. Adv. Neural. Inf. Process. Syst. 36, 5685\u20135705 (2023)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Zhao, H., Zeng, X., Chen, T., Liu, Z.: Synthesizing barrier certificates using neural networks. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2020)","DOI":"10.1145\/3365365.3382222"},{"key":"4_CR36","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 the 25th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2022)","DOI":"10.1145\/3501710.3519511"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05435-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:43:22Z","timestamp":1766043802000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05435-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032054340","9783032054357"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05435-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Graz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","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":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","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":"rv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv25.isec.tugraz.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}