{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:08:07Z","timestamp":1779034087451,"version":"3.51.4"},"publisher-location":"Cham","reference-count":44,"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                    Branch and Bound (\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt{BaB}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>BaB<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt{BaB}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>BaB<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    lies in searching for the\n                    <jats:italic>verdict boundaries<\/jats:italic>\n                    across all the paths that divide the verified and unverified subproblems. We observe that the existing\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt{BaB}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>BaB<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt{BaB}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>BaB<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary\u2019s position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\texttt{BaB}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>BaB<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -based approaches.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_4","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:52Z","timestamp":1779033052000},"page":"67-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mining Verdict Boundaries for\u00a0Neural Network Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7635-468X","authenticated-orcid":false,"given":"Jiawei","family":"Ren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3844-8180","authenticated-orcid":false,"given":"Guanqin","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9510-6574","authenticated-orcid":false,"given":"Yulei","family":"Sui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Bentley, J.L., Yao, A.C.C.: An almost optimal algorithm for unbounded searching. Inform. Process. Lett. 5(SLAC-PUB-1679) (1976). https:\/\/doi.org\/10.1016\/0020-0190(76)90071-5","DOI":"10.1016\/0020-0190(76)90071-5"},{"issue":"4","key":"4_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3617508","volume":"23","author":"F Boudardara","year":"2024","unstructured":"Boudardara, F., Boussif, A., Meyer, P.J., Ghazel, M.: A review of abstraction methods toward verifying neural networks. ACM Trans. Embedded Comput. Syst. 23(4), 1\u201319 (2024). https:\/\/doi.org\/10.1145\/3617508","journal-title":"ACM Trans. Embedded Comput. Syst."},{"key":"4_CR3","unstructured":"Brix, C., Bak, S., Liu, C., Johnson, T.T.: 4th int. verification of neural networks competition (vnn-comp 2023): Summary and results. arXiv preprint arXiv:2312.16760 (2023)"},{"key":"4_CR4","unstructured":"Bunel, R., et al.: Lagrangian decomposition for neural network verification. In: Conference on Uncertainty in Artificial Intelligence, pp. 370\u2013379. PMLR (2020). http:\/\/proceedings.mlr.press\/v124\/bunel20a.html"},{"key":"4_CR5","unstructured":"Bunel, R., Mudigonda, P., Turkaslan, I., Torr, P., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21(2020) (2020), https:\/\/jmlr.org\/papers\/v21\/19-468.html"},{"key":"4_CR6","unstructured":"Cohen, E., Elboher, Y.Y., Barrett, C., Katz, G.: Tighter abstract queries in neural network verification. arXiv preprint arXiv:2210.12871 (2022)"},{"key":"4_CR7","unstructured":"Dalrymple, D., et\u00a0al.: Towards guaranteed safe ai: A framework for ensuring robust and reliable ai systems. arXiv preprint arXiv:2405.06624 (2024)"},{"key":"4_CR8","unstructured":"De\u00a0Palma, A., et al.: Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718 (2021)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","volume-title":"Automated Technology for Verification and Analysis","author":"R Ehlers","year":"2017","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269\u2013286. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Fukuda, K., Zhang, G., Zhang, Z., Sui, Y., Zhao, J.: Adaptive branch-and-bound tree exploration for neural network verification. In: 2025 Design, Automation & Test in Europe Conference (DATE), pp.\u00a01\u20137 (2025). https:\/\/doi.org\/10.23919\/DATE64628.2025.10992738","DOI":"10.23919\/DATE64628.2025.10992738"},{"key":"4_CR11","unstructured":"Geng, C., Le, N., Xu, X., Wang, Z., Gurfinkel, A., Si, X.: Towards reliable neural specifications. In: International Conference on Machine Learning, pp. 11196\u201311212. PMLR (2023). https:\/\/proceedings.mlr.press\/v202\/geng23a.html"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: 3rd Int. Conf. on Learning Representations (ICLR 2015). Int. Conf. on Learning Representations, ICLR, San Diego, CA, United States (2015). https:\/\/doi.org\/10.48550\/arXiv.1412.6572","DOI":"10.48550\/arXiv.1412.6572"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Guo, X., Wan, W., Zhang, Z., Zhang, M., Song, F., Wen, X.: Eager falsification for accelerating robustness verification of deep neural networks. In: 2021 IEEE 32nd Int. Symp. on Software Reliability Engineering (ISSRE), pp. 345\u2013356. IEEE (2021). https:\/\/doi.org\/10.1109\/ISSRE52982.2021.00044","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Henriksen, P., Lomuscio, A.: Deepsplit: an efficient splitting method for neural network verification via indirect effect analysis. In: IJCAI, pp. 2549\u20132555 (2021). https:\/\/doi.org\/10.24963\/ijcai.2021\/351","DOI":"10.24963\/ijcai.2021\/351"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Lukina, A., Schilling, C.: Outside the box: abstraction-based monitoring of neural networks. In: ECAI 2020, pp. 2433\u20132440. IOS Press (2020). https:\/\/doi.org\/10.48550\/arXiv.1911.09032","DOI":"10.48550\/arXiv.1911.09032"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., Barrett, C.: Towards efficient verification of quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a038, pp. 21152\u201321160 (2024). https:\/\/doi.org\/10.1609\/aaai.v38i19.30108","DOI":"10.1609\/aaai.v38i19.30108"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","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., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"4_CR18","unstructured":"Isac, O., Zohar, Y., Barrett, C., Katz, G.: Dnn verification, reachability, and the exponential function problem. arXiv preprint arXiv:2305.06064 (2023)"},{"key":"4_CR19","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":"4_CR20","doi-asserted-by":"publisher","unstructured":"Liu, C., et\u00a0al.: Algorithms for verifying deep neural networks. Foundat. Trends\u00ae Optimizat. 4(3-4), 244\u2013404 (2021). https:\/\/doi.org\/10.1561\/2400000035","DOI":"10.1561\/2400000035"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-030-88494-9_3","volume-title":"Runtime Verification","author":"A Lukina","year":"2021","unstructured":"Lukina, A., Schilling, C., Henzinger, T.A.: Into the unknown: active monitoring of\u00a0neural networks. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 42\u201361. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_3"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: 6th Int. Conf. on Learning Representations (ICLR 2018), Vancouver, Canada (2018). https:\/\/doi.org\/10.48550\/arXiv.1706.06083","DOI":"10.48550\/arXiv.1706.06083"},{"key":"4_CR23","unstructured":"Mandal, U., et\u00a0al.: Formally verifying deep reinforcement learning controllers with lyapunov barrier certificates. arXiv preprint arXiv:2405.14058 (2024)"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Mitra, S., et al.: Formal verification techniques for vision-based autonomous systems\u2013a survey. In: Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, pp. 89\u2013108. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_5","DOI":"10.1007\/978-3-031-75778-5_5"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Ostrovsky, M., Barrett, C., Katz, G.: An abstraction-refinement approach to verifying convolutional neural networks. In: International Symposium on Automated Technology for Verification and Analysis, pp. 391\u2013396. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_25","DOI":"10.1007\/978-3-031-19992-9_25"},{"key":"4_CR26","unstructured":"Ren, J.: Artifact: \"mining verdict boundaries for neural network verification\". GitHub (2026). https:\/\/github.com\/jiawei-95\/BMiner"},{"key":"4_CR27","unstructured":"Shi, Z., Wang, Y., Zhang, H., Kolter, J.Z., Hsieh, C.J.: Efficiently computing local lipschitz constants of neural networks via bound propagation. Adv. Neural Inform. Process. Syst. 35, 2350\u20132364 (2022). http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/0ff54b4ec4f70b3ae12c8621ca8a49f4-Abstract-Conference.html"},{"key":"4_CR28","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. Adv. Neural Inform. Process. Syst. 31 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/f2f446980d8e971ef3da97af089481c3-Abstract.html"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. ACM Program. Lang. 3(POPL), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"issue":"10","key":"4_CR30","doi-asserted-by":"publisher","first-page":"3685","DOI":"10.1007\/s10994-021-06050-2","volume":"112","author":"CA Strong","year":"2023","unstructured":"Strong, C.A., et al.: Global optimization of objective functions represented by relu networks. Mach. Learn. 112(10), 3685\u20133712 (2023). https:\/\/doi.org\/10.1007\/s10994-021-06050-2","journal-title":"Mach. Learn."},{"key":"4_CR31","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Int. Conf. on Learning Representations (2018). https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"4_CR32","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. Adv. Neural Inform. Process, Syst. 31 (2018), https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html"},{"key":"4_CR33","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symp. (USENIX Security 2018), pp. 1599\u20131614 (2018). https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"4_CR34","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. Adv. Neural Inform. Process. Syst. 34, 29909\u201329921 (2021). https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/fac7fead96dafceaf80c1daffeae82a4-Abstract.html"},{"key":"4_CR35","unstructured":"Wei, D., Wu, H., Wu, M., Chen, P.Y., Barrett, C., Farchi, E.: Convex bounds on the softmax function with applications to robustness verification. In: International Conference on Artificial Intelligence and Statistics, pp. 6853\u20136878. PMLR (2023). https:\/\/proceedings.mlr.press\/v206\/wei23c.html"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Wu, H., et al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 249\u2013264. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_13","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Wu, H., et al.: Toward certified robustness against real-world distribution shifts. In: 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML), pp. 537\u2013553. IEEE (2023). https:\/\/doi.org\/10.1109\/SaTML54575.2023.00042","DOI":"10.1109\/SaTML54575.2023.00042"},{"key":"4_CR38","unstructured":"Wu, M., Wu, H., Barrett, C.: Verix: towards verified explainability of deep neural networks. Adv. Neural Inform. Process. Syst. 36 (2024). http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/46907c2ff9fafd618095161d76461842-Abstract-Conference.html"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural networks. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, pp. 3622\u20133628. International Joint Conferences on Artificial Intelligence Organization (7 2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/503, main Track","DOI":"10.24963\/ijcai.2022\/503"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Zelazny, T., Wu, H., Barrett, C., Katz, G.: On optimizing back-substitution methods for neural network verification. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 17\u201326. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_7","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_7"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Zhang, G., et al.: Efficient neural network verification via order leading exploration of branch-and-bound trees. In: 39th European Conference on Object-Oriented Programming (ECOOP 2025), vol.\u00a0333, pp. 36:1\u201336:29 (2025). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2025.36","DOI":"10.4230\/LIPIcs.ECOOP.2025.36"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Zhang, H., Shinn, M., Gupta, A., Gurfinkel, A., Le, N., Narodytska, N.: Verification of recurrent neural networks for cognitive tasks via reachability analysis. In: ECAI 2020, pp. 1690\u20131697. IOS Press (2020). https:\/\/doi.org\/10.3233\/FAIA200281","DOI":"10.3233\/FAIA200281"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Zhang, R., Sun, J.: Certified robust accuracy of neural networks are bounded due to bayes errors. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 352\u2013376. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_18","DOI":"10.1007\/978-3-031-65630-9_18"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Chen, G., Song, F., Sun, J., Dong, J.S.L: Certified quantization strategy synthesis for neural networks. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) FM 2024. LNCS, vol. 14933. Springer, Cham . (2025). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_18","DOI":"10.1007\/978-3-031-71162-6_18"}],"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_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:56Z","timestamp":1779033056000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_4","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"}}]}}