{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T09:27:31Z","timestamp":1780392451411,"version":"3.54.1"},"publisher-location":"Singapore","reference-count":49,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819542123","type":"print"},{"value":"9789819542130","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"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-981-95-4213-0_1","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:15Z","timestamp":1762816695000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of\u00a0Physical Layer Security Protocols for\u00a0Next-Generation Communication Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2460-7926","authenticated-orcid":false,"given":"Kangfeng","family":"Ye","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6992-4285","authenticated-orcid":false,"given":"Roberto","family":"Metere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7955-2702","authenticated-orcid":false,"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0169-0704","authenticated-orcid":false,"given":"Poonam","family":"Yadav","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Arapinis, M., et al.: New privacy issues in mobile telephony: fix and verification. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS 2012, pp. 205\u2013216. Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2382196.2382221","DOI":"10.1145\/2382196.2382221"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_27"},{"issue":"4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/3157831.3157835","volume":"4","author":"D Basin","year":"2017","unstructured":"Basin, D., Cremers, C., Dreier, J., Sasse, R.: Symbolically analyzing security protocols using tamarin. ACM SIGLOG News 4(4), 19\u201330 (2017). https:\/\/doi.org\/10.1145\/3157831.3157835","journal-title":"ACM SIGLOG News"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Basin, D., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real world, cryptographic protocols. IEEE Secur. Priv. Mag. (2022). https:\/\/doi.org\/10.1109\/msec.2022.3154689. https:\/\/hal.science\/hal-03586826","DOI":"10.1109\/msec.2022.3154689"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Basin, D., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, pp. 1383\u20131396. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3243734.3243846","DOI":"10.1145\/3243734.3243846"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy (SP). IEEE (2017). https:\/\/doi.org\/10.1109\/sp.2017.26","DOI":"10.1109\/sp.2017.26"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/3-540-48892-8_26","volume-title":"Selected Areas in Cryptography","author":"S Blake-Wilson","year":"1999","unstructured":"Blake-Wilson, S., Menezes, A.: Authenticated Diffe-Hellman key agreement protocols. In: Tavares, S., Meijer, H. (eds.) SAC 1998. LNCS, vol. 1556, pp. 339\u2013361. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48892-8_26"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends\u00ae Priv. Secur. 1(1\u20132), 1\u2013135 (2016). https:\/\/doi.org\/10.1561\/3300000004","DOI":"10.1561\/3300000004"},{"key":"1_CR9","unstructured":"Boichut, Y., Genet, T., Glouche, Y., Heen, O.: Using animation to improve formal specifications of security protocols. In: 2nd Conference on Security in Network Architectures and Information Systems (SARSSI 2007), pp. 169\u2013182 (2007)"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Costa, G., Degano, P., Galletta, L., Soderi, S.: Formally verifying security protocols built on watermarking and jamming. Comput. Secur. 128, 103133 (2023). https:\/\/doi.org\/10.1016\/j.cose.2023.103133. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167404823000433","DOI":"10.1016\/j.cose.2023.103133"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Cox, I., Miller, M., McKellips, A.: Watermarking as communications with side information. Proc. IEEE 87(7), 1127\u20131141 (1999). https:\/\/doi.org\/10.1109\/5.771068. https:\/\/ieeexplore.ieee.org\/document\/771068","DOI":"10.1109\/5.771068"},{"issue":"1","key":"1_CR12","first-page":"48","volume":"32","author":"I Csisz\u00e1r","year":"1996","unstructured":"Csisz\u00e1r, I.: Almost independence and secrecy capacity. Probl. Peredachi Inf. 32(1), 48\u201357 (1996)","journal-title":"Probl. Peredachi Inf."},{"issue":"6","key":"1_CR13","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976). https:\/\/doi.org\/10.1109\/TIT.1976.1055638","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"1\u20132","key":"1_CR15","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoret. Comput. Sci. 367(1\u20132), 162\u2013202 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.035","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Foster, S., Hur, C.K., Woodcock, J.: Formally verified simulations of state-rich processes using interaction trees in Isabelle\/HOL. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0203, pp. 20:1\u201320:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.20. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CONCUR.2021.20","DOI":"10.4230\/LIPIcs.CONCUR.2021.20"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Gollakota, S., Katabi, D.: Physical layer wireless security made fast and channel independent. In: 2011 Proceedings IEEE INFOCOM, pp. 1125\u20131133 (2011). https:\/\/doi.org\/10.1109\/INFCOM.2011.5934889. https:\/\/ieeexplore.ieee.org\/document\/5934889","DOI":"10.1109\/INFCOM.2011.5934889"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"key":"1_CR20","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Int. (1985)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-540-45146-4_24","volume-title":"Advances in Cryptology - CRYPTO 2003","author":"H Krawczyk","year":"2003","unstructured":"Krawczyk, H.: SIGMA: the \u2018SIGn-and-MAc\u2019 approach to authenticated Diffie-Hellman and its use in the IKE protocols. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 400\u2013425. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45146-4_24"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/11535218_33","volume-title":"Advances in Cryptology \u2013 CRYPTO 2005","author":"H Krawczyk","year":"2005","unstructured":"Krawczyk, H.: HMQV: a high-performance secure Diffie-Hellman protocol. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 546\u2013566. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11535218_33"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Kumar, M.S., Ramanathan, R., Jayakumar, M.: Key less physical layer security for wireless networks: a survey. Eng. Sci. Technol. Int. J. 35, 101260 (2022). https:\/\/doi.org\/10.1016\/j.jestch.2022.101260. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S2215098622001690","DOI":"10.1016\/j.jestch.2022.101260"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Li, X., Yu, C., Hizlan, M., Kim, W.T., Park, S.: Physical layer watermarking of direct sequence spread spectrum signals. In: MILCOM 2013 - 2013 IEEE Military Communications Conference, pp. 476\u2013481. IEEE, San Diego, CA, USA (2013). https:\/\/doi.org\/10.1109\/MILCOM.2013.88. http:\/\/ieeexplore.ieee.org\/document\/6735668\/","DOI":"10.1109\/MILCOM.2013.88"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. In: Proceedings 10th Computer Security Foundations Workshop, pp. 18\u201330 (1997). https:\/\/doi.org\/10.1109\/CSFW.1997.596779. https:\/\/ieeexplore.ieee.org\/document\/596779","DOI":"10.1109\/CSFW.1997.596779"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147\u2013166. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_43"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Menezes, A.J., Vanstone, S.A., Oorschot, P.C.V.: Handbook of Applied Cryptography, 1st edn. CRC Press, Inc., USA (1996). https:\/\/doi.org\/10.1201\/9780429466335","DOI":"10.1201\/9780429466335"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Metere, R., Arnaboldi, L.: Automating cryptographic protocol language generation from structured specifications. In: Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering, pp. 91\u2013101 (2022). https:\/\/doi.org\/10.1145\/3524482.35276","DOI":"10.1145\/3524482.35276"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Miller, R., Boureanu, I., Wesemeyer, S., Newton, C.J.P.: The 5G key-establishment stack: in-depth formal verification and experimentation. In: Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security, ASIA CCS 2022, pp. 237\u2013251. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3488932.3517421","DOI":"10.1145\/3488932.3517421"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Mitev, M., Chorti, A., Poor, H.V., Fettweis, G.P.: What physical layer security can do for 6G security. IEEE Open J. Veh. Technol. 4, 375\u2013388 (2023). https:\/\/doi.org\/10.1109\/OJVT.2023.3245071. https:\/\/ieeexplore.ieee.org\/document\/10044975\/?arnumber=10044975","DOI":"10.1109\/OJVT.2023.3245071"},{"issue":"5","key":"1_CR31","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: Robochart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00710-z","journal-title":"Softw. Syst. Model."},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). https:\/\/doi.org\/10.1145\/359657.359659. https:\/\/dl.acm.org\/doi\/10.1145\/359657.359659","DOI":"10.1145\/359657.359659"},{"issue":"4","key":"1_CR33","doi-asserted-by":"publisher","first-page":"2384","DOI":"10.1109\/COMST.2021.3108618","volume":"23","author":"VL Nguyen","year":"2021","unstructured":"Nguyen, V.L., Lin, P.C., Cheng, B.C., Hwang, R.H., Lin, Y.D.: Security and privacy for 6G: a survey on prospective technologies and challenges. IEEE Commun. Surv. Tutor. 23(4), 2384\u20132428 (2021). https:\/\/doi.org\/10.1109\/COMST.2021.3108618","journal-title":"IEEE Commun. Surv. Tutor."},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Paulson, L.C.: Mechanized proofs of security protocols: Needham-Schroeder with public keys. Technical report, University of Cambridge (1997). https:\/\/doi.org\/10.48456\/tr-413","DOI":"10.48456\/tr-413"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer (2011). https:\/\/doi.org\/10.1007\/978-1-84882-258-0","DOI":"10.1007\/978-1-84882-258-0"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Shannon, C.E.: A mathematical theory of communication. Bell Syst. Tech. J. 27(3), 379\u2013423 (1948). https:\/\/doi.org\/10.1002\/j.1538-7305.1948.tb01338.x. https:\/\/ieeexplore.ieee.org\/document\/6773024\/?arnumber=6773024","DOI":"10.1002\/j.1538-7305.1948.tb01338.x"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings 35th Annual Symposium on Foundations of Computer Science, pp. 124\u2013134 (1994). https:\/\/doi.org\/10.1109\/SFCS.1994.365700","DOI":"10.1109\/SFCS.1994.365700"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Soderi, S., Brighente, A., Turrin, F., Conti, M.: VLC physical layer security through RIS-aided jamming receiver for 6G wireless networks. In: 2022 19th Annual IEEE International Conference on Sensing, Communication, and Networking (SECON), pp. 370\u2013378 (2022). https:\/\/doi.org\/10.1109\/SECON55815.2022.9918547. http:\/\/arxiv.org\/abs\/2205.09026","DOI":"10.1109\/SECON55815.2022.9918547"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Soderi, S., De\u00a0Nicola, R.: 6G networks physical layer security using RGB visible light communications. IEEE Access 10, 5482\u20135496 (2022). https:\/\/doi.org\/10.1109\/ACCESS.2021.3139456","DOI":"10.1109\/ACCESS.2021.3139456"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Soderi, S., Mucchi, L., H\u00e4m\u00e4l\u00e4inen, M., Piva, A., Iinatti, J.: Physical layer security based on spread-spectrum watermarking and jamming receiver. Trans. Emerg. Telecommun. Technol. 28(7), e3142 (2017). https:\/\/doi.org\/10.1002\/ett.3142. https:\/\/onlinelibrary.wiley.com\/doi\/abs\/10.1002\/ett.3142","DOI":"10.1002\/ett.3142"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Wyner, A.D.: The wire-tap channel. Bell Syst. Tech. J. 54(8), 1355\u20131387 (1975). https:\/\/doi.org\/10.1002\/j.1538-7305.1975.tb02040.x. https:\/\/ieeexplore.ieee.org\/document\/6772207","DOI":"10.1002\/j.1538-7305.1975.tb02040.x"},{"key":"1_CR43","unstructured":"Xia, L.Y.: Executable denotational semantics with interaction trees. Ph.D. thesis, University of Pennsylvania (2022)"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Xia, L.Y., et al.: Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371119","DOI":"10.1145\/3371119"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Ye, K., Cavalcanti, A., Foster, S., Miyazawa, A., Woodcock, J.: Probabilistic modelling and verification using RoboChart and PRISM. Softw. Syst. Model. 21(2), 667\u2013716 (2022). https:\/\/doi.org\/10.1007\/s10270-021-00916-8","DOI":"10.1007\/s10270-021-00916-8"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Ye, K., Foster, S., Woodcock, J.: Formally verified animation for RoboChart using interaction trees. J. Log. Algebraic Methods Program. 137, 100940 (2024). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100940","DOI":"10.1016\/j.jlamp.2023.100940"},{"key":"1_CR47","unstructured":"Ye, K., Metere, R., Woodcock, J., Yadav, P.: Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) (2025). https:\/\/arxiv.org\/abs\/2508.19430"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"Ye, K., Metere, R., Yadav, P.: User-guided verification of security protocols via sound animation. In: Software Engineering and Formal Methods, pp. 33\u201351. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-77382-2_3","DOI":"10.1007\/978-3-031-77382-2_3"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"Zhang, S., Zhu, D., Liu, Y.: Artificial intelligence empowered physical layer security for 6G: state-of-the-art, challenges, and opportunities. Comput. Netw. 242, 110255 (2024). https:\/\/doi.org\/10.1016\/j.comnet.2024.110255. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1389128624000872","DOI":"10.1016\/j.comnet.2024.110255"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:17Z","timestamp":1762816697000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","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":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}