{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:49:59Z","timestamp":1760042999580,"version":"3.40.3"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711619"},{"type":"electronic","value":"9783031711626"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Quantization plays an important role in deploying neural networks on embedded, real-time systems with limited computing and storage resources (e.g., edge devices). It significantly reduces the model storage cost and improves inference efficiency by using fewer bits to represent the parameters. However, it was recently shown that critical properties may be broken after quantization, such as robustness and backdoor-freeness. In this work, we introduce the first method for synthesizing quantization strategies that verifiably maintain desired properties after quantization, leveraging a key insight that quantization leads to a data distribution shift in each layer. We propose to compute the preimage for each layer based on which the preceding layer is quantized, ensuring that the quantized reachable region of the preceding layer remains within the preimage. To tackle the challenge of computing the exact preimage, we propose an MILP-based method to compute its under-approximation. We implement our method into a tool and demonstrate its effectiveness and efficiency by providing certified quantization that successfully preserves model robustness and backdoor-freeness.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_18","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"343-362","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Certified Quantization Strategy Synthesis for\u00a0Neural Networks"],"prefix":"10.1007","author":[{"given":"Yedi","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Guangke","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 1\u201339 (2018)","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-39799-8_22","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 313\u2013329. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_22"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Amir, G., Wu, H., Barrett, C.W., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 12652, pp. 203\u2013222 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_11","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Dathathri, S., Gao, S., Murray, R.M.: Inverse abstraction of neural networks using symbolic interpolation. In: Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI), pp. 3437\u20133444 (2019). https:\/\/doi.org\/10.1609\/AAAI.V33I01.33013437","DOI":"10.1609\/AAAI.V33I01.33013437"},{"key":"18_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/J.COSREV.2021.100379","volume":"40","author":"S Dong","year":"2021","unstructured":"Dong, S., Wang, P., Abbas, K.: A survey on deep learning and its applications. Comput. Sci. Rev. 40, 100379 (2021). https:\/\/doi.org\/10.1016\/J.COSREV.2021.100379","journal-title":"Comput. Sci. Rev."},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Eleftheriadis, C., Kekatos, N., Katsaros, P., Tripakis, S.: On neural network equivalence checking using SMT solvers. In: Proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems, vol. 13465, pp. 237\u2013257 (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_14","DOI":"10.1007\/978-3-031-15839-1_14"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI$$^2$$: safety and robustness certification of neural networks with abstract interpretation. In: Proceedings of the 2018 IEEE Symposium on Security and Privacy, pp. 3\u201318 (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Gholami, A., Kim, S., Dong, Z., Yao, Z., Mahoney, M.W., Keutzer, K.: A survey of quantization methods for efficient neural network inference. In: Low-Power Computer Vision, pp. 291\u2013326. Chapman and Hall\/CRC (2022)","DOI":"10.1201\/9781003162810-13"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-45237-7_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Giacobbe","year":"2020","unstructured":"Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quantize your neural network? In: TACAS 2020. LNCS, vol. 12079, pp. 79\u201397. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_5"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Guo, X., Wan, W., Zhang, Z., Zhang, M., Song, F., Wen, X.: Eager falsification for accelerating robustness verification of deep neural networks. In: Proceedings of the 32nd IEEE International Symposium on Software Reliability Engineering, pp. 345\u2013356 (2021)","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"18_CR11","unstructured":"Gurobi. A most powerful mathematical optimization solver (2018). https:\/\/www.gurobi.com\/"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Lechner, M., Zikelic, D.: Scalable verification of quantized neural networks. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI), pp. 3787\u20133795 (2021). https:\/\/doi.org\/10.1609\/AAAI.V35I5.16496","DOI":"10.1609\/AAAI.V35I5.16496"},{"key":"18_CR13","unstructured":"Hong, S., Panaitescu-Liess, M., Kaya, Y., Dumitras, T.: Qu-anti-zation: exploiting quantization artifacts for achieving adversarial outcomes. In: Proceedings of the Annual Conference on Neural Information Processing Systems (NeurIPS), pp. 9303\u20139316 (2021)"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Huang, P., et al.: Towards efficient verification of quantized neural networks. In: Proceedings of the 38th AAAI Conference on Artificial Intelligence, pp. 21152\u201321160 (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I19.30108","DOI":"10.1609\/AAAI.V38I19.30108"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Jacob, B., et al.: Quantization and training of neural networks for efficient integer-arithmetic-only inference. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 2704\u20132713 (2018)","DOI":"10.1109\/CVPR.2018.00286"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Jr., J.B.P.M., de\u00a0Lima\u00a0Filho, E.B., Bessa, I., Manino, E., Song, X., Cordeiro, L.C.: Counterexample guided neural network quantization refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 43(4), 1121\u20131134 (2024). https:\/\/doi.org\/10.1109\/TCAD.2023.3335313","DOI":"10.1109\/TCAD.2023.3335313"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proceedings of the 29th International Conference on Computer Aided Verification, pp. 97\u2013117 (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"18_CR18","unstructured":"Kotha, S., Brix, C., Kolter, J.Z., Dvijotham, K., Zhang, H.: Provably bounding neural network preimages. Adv. Neural Inf. Process. Syst. 36 (2024)"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Lechner, M., \u017dikeli\u0107, \u0110., Chatterjee, K., Henzinger, T.A., Rus, D.: Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), pp. 14964\u201314973 (2023). https:\/\/doi.org\/10.1609\/AAAI.V37I12.26747","DOI":"10.1609\/AAAI.V37I12.26747"},{"key":"18_CR20","unstructured":"LeCun, Y., Cortes, C.: Mnist handwritten digit database (2010)"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Li, Z., Ni, B., Zhang, W., Yang, X., Gao, W.: Performance guaranteed network acceleration via high-order residual quantization. In: IEEE International Conference on Computer Vision (ICCV), pp. 2603\u20132611 (2017). https:\/\/doi.org\/10.1109\/ICCV.2017.282","DOI":"10.1109\/ICCV.2017.282"},{"key":"18_CR22","unstructured":"Lin, D.D., Talathi, S.S., Annapureddy, V.S.: Fixed point quantization of deep convolutional networks. In: Proceedings of the 33nd International Conference on Machine Learning (ICML). pp. 2849\u20132858 (2016)"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Lin, H., Lou, J., Xiong, L., Shahabi, C.: Integer-arithmetic-only certified robustness for quantized neural networks. In: Proceedings of the IEEE\/CVF International Conference on Computer Vision (CVPR), pp. 7808\u20137817. IEEE (2021). https:\/\/doi.org\/10.1109\/ICCV48922.2021.00773","DOI":"10.1109\/ICCV48922.2021.00773"},{"key":"18_CR24","unstructured":"Lin, J., Gan, C., Han, S.: Defensive quantization: when efficiency meets robustness. In: International Conference on Learning Representations (2018)"},{"key":"18_CR25","unstructured":"Liu, J., Xing, Y., Shi, X., Song, F., Xu, Z., Ming, Z.: Abstraction and refinement: towards scalable and exact verification of neural networks. arXiv preprint arXiv:2207.00759 (2022)"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Ma, H., et al.: Quantization backdoors to deep learning commercial frameworks. IEEE Trans. Depend Secure Comput. (2023). https:\/\/doi.org\/10.1109\/TDSC.2023.3271956","DOI":"10.1109\/TDSC.2023.3271956"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Marco, V.S., Taylor, B., Wang, Z., Elkhatib, Y.: Optimizing deep learning inference on embedded systems through adaptive model selection. ACM Trans. Embed. Comput. Syst. 19(1), 2:1\u20132:28 (2020). https:\/\/doi.org\/10.1145\/3371154","DOI":"10.1145\/3371154"},{"key":"18_CR28","unstructured":"Matoba, K., Fleuret, F.: Exact preimages of neural network aircraft collision avoidance systems. In: Proceedings of the Workshop on Machine Learning for Engineering Modeling, Simulation, and Design, pp.\u00a01\u20139 (2020)"},{"key":"18_CR29","unstructured":"Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Proceedings of the 35th International Conference on Machine Learning, vol.\u00a080, pp. 3575\u20133583 (2018)"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-030-85037-1_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Mohammadinejad","year":"2021","unstructured":"Mohammadinejad, S., Paulsen, B., Deshmukh, J.V., Wang, C.: DiffRNN: differential verification of recurrent neural networks. In: Dima, C., Shirmohammadi, M. (eds.) FORMATS 2021. LNCS, vol. 12860, pp. 117\u2013134. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85037-1_8"},{"issue":"6","key":"18_CR31","doi-asserted-by":"publisher","first-page":"199","DOI":"10.3390\/FI15060199","volume":"15","author":"AA Musa","year":"2023","unstructured":"Musa, A.A., Hussaini, A., Liao, W., Liang, F., Yu, W.: Deep neural networks for spatial-temporal cyber-physical systems: a survey. Future Internet 15(6), 199 (2023). https:\/\/doi.org\/10.3390\/FI15060199","journal-title":"Future Internet"},{"key":"18_CR32","unstructured":"Nagel, M., Amjad, R.A., Van\u00a0Baalen, M., Louizos, C., Blankevoort, T.: Up or down? Adaptive rounding for post-training quantization. In: Proceedings of the 37th International Conference on Machine Learning (ICML), vol.\u00a0119, pp. 7197\u20137206 (2020)"},{"key":"18_CR33","unstructured":"Nagel, M., Fournarakis, M., Amjad, R.A., Bondarenko, Y., van Baalen, M., Blankevoort, T.: A white paper on neural network quantization. arXiv preprint arXiv:2106.08295 (2021)"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Pan, X., Zhang, M., Yan, Y., Yang, M.: Understanding the threats of trojaned quantized neural network in model supply chains. In: Proceedings of the Annual Computer Security Applications Conference (ACSAC), pp. 634\u2013645 (2021). https:\/\/doi.org\/10.1145\/3485832.3485881","DOI":"10.1145\/3485832.3485881"},{"key":"18_CR35","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, C.: Reludiff: differential verification of deep neural networks. In: 2020 IEEE\/ACM 42nd International Conference on Software Engineering (ICSE), pp. 714\u2013726. IEEE (2020)","DOI":"10.1145\/3377811.3380337"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, J., Wang, C.: NeuroDiff: scalable differential verification of neural networks using fine-grained approximation. In: Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering, pp. 784\u2013796 (2020)","DOI":"10.1145\/3324884.3416560"},{"key":"18_CR37","doi-asserted-by":"publisher","unstructured":"Pham, L.H., Sun, J.: Verifying neural networks against backdoor attacks. In: Proceedings of the 34th International Conference on Computer Aided Verification (CAV), pp. 171\u2013192 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_9","DOI":"10.1007\/978-3-031-13185-1_9"},{"key":"18_CR38","unstructured":"Prabhakar, P., Afzal, Z.R.: Abstraction based output range analysis for neural networks. In: Proceedings of the Annual Conference on Neural Information Processing Systems, pp. 15762\u201315772 (2019)"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Rokh, B., Azarpeyvand, A., Khanteymoori, A.: A comprehensive survey on model quantization for deep neural networks in image classification. ACM Trans. Intell. Syst. Technol. 14(6), 97:1\u201397:50 (2023). https:\/\/doi.org\/10.1145\/3623402","DOI":"10.1145\/3623402"},{"key":"18_CR40","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. (POPL) 3, 41:1\u201341:30 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"18_CR41","unstructured":"Song, C., Fallon, E., Li, H.: Improving adversarial robustness in weight-quantized neural networks. arXiv preprint arXiv:2012.14965 (2020)"},{"key":"18_CR42","doi-asserted-by":"crossref","unstructured":"Song, X., Sun, Y., Mustafa, M.A., Cordeiro, L.C.: QNNRepair: qneural network repair. In: Proceedings of the 21st International Conference on Software Engineering and Formal Methods, vol. 14323, pp. 320\u2013339 (2023)","DOI":"10.1007\/978-3-031-47115-5_18"},{"key":"18_CR43","unstructured":"Tang, Z., Dong, Y., Su, H.: Error-silenced quantization: bridging robustness and compactness. In: Proceedings of the Workshop on Artificial Intelligence Safety (AISafety@IJCAI) (2020)"},{"key":"18_CR44","doi-asserted-by":"publisher","unstructured":"Wang, P., Hu, Q., Zhang, Y., Zhang, C., Liu, Y., Cheng, J.: Two-step quantization for low-bit neural networks. In: Proceedings of the IEEE\/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pp. 4376\u20134384 (2018). https:\/\/doi.org\/10.1109\/CVPR.2018.00460","DOI":"10.1109\/CVPR.2018.00460"},{"key":"18_CR45","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Proceedings of the Annual Conference on Neural Information Processing Systems, pp. 29909\u201329921 (2021)"},{"key":"18_CR46","unstructured":"Xiao, H., Rasul, K., Vollgraf, R.: Fashion-MNIST: a novel image dataset for benchmarking machine learning algorithms. arXiv preprint arXiv:1708.07747 (2017)"},{"key":"18_CR47","doi-asserted-by":"publisher","unstructured":"Yang, P., et al.: Improving neural network verification through spurious region guided refinement. In: TACAS 2021. LNCS, vol. 12651, pp. 389\u2013408. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_21","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"18_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-030-01237-3_23","volume-title":"Computer Vision \u2013 ECCV 2018","author":"D Zhang","year":"2018","unstructured":"Zhang, D., Yang, J., Ye, D., Hua, G.: LQ-Nets: learned quantization for highly accurate and compact deep neural networks. In: Ferrari, V., Hebert, M., Sminchisescu, C., Weiss, Y. (eds.) ECCV 2018. LNCS, vol. 11212, pp. 373\u2013390. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01237-3_23"},{"key":"18_CR49","unstructured":"Zhang, X., Wang, B., Kwiatkowska, M.: On preimage approximation for neural networks. arXiv preprint arXiv:2305.03686 (2023)"},{"key":"18_CR50","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Chen, G., Song, F., Sun, J., Dong, J.S.: Certified quantization strategy synthesis for neural networks. https:\/\/github.com\/zhangyedi\/Quadapter (2024)","DOI":"10.1007\/978-3-031-71162-6_18"},{"key":"18_CR51","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Song, F., Sun, J.: Qebverif: quantization error bound verification of neural networks. In: Proceedings of the 35th International Conference on Computer Aided Verification, vol. 13965, pp. 413\u2013437 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_20","DOI":"10.1007\/978-3-031-37703-7_20"},{"key":"18_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-030-81685-8_8","volume-title":"Computer Aided Verification","author":"Y Zhang","year":"2021","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: BDD4BNN: a BDD-based quantitative analysis framework for binarized neural networks. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 175\u2013200. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_8"},{"key":"18_CR53","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: Precise quantitative analysis of binarized neural networks: a BDD-based approach. ACM Trans. Softw. Eng. Methodol. 32(3), 62:1\u201362:51 (2023). https:\/\/doi.org\/10.1145\/3563212","DOI":"10.1145\/3563212"},{"key":"18_CR54","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Zhang, M., Chen, T., Sun, J.: Qvip: an ilp-based formal verification approach for quantized neural networks. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 82:1\u201382:13 (2022). https:\/\/doi.org\/10.1145\/3551349.3556916","DOI":"10.1145\/3551349.3556916"},{"key":"18_CR55","unstructured":"Zhu, Y., et al.: Towards robustness evaluation of backdoor defense on quantized deep learning model. SSRN: https:\/\/ssrn.com\/abstract=4578346"}],"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-031-71162-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T23:02:10Z","timestamp":1732748530000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}