{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:29:55Z","timestamp":1768213795109,"version":"3.49.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-15700-3_16","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:48Z","timestamp":1768202508000},"page":"335-358","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Executable Semantics of\u00a0PROMELA"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6482-1789","authenticated-orcid":false,"given":"Byoungho","family":"Son","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Bae, K., Escobar, S., L\u00f3pez-Rueda, R., Meseguer, J., Sapi\u00f1a, J.: Verifying invariants by deductive model checking. In: International Workshop on Rewriting Logic and Its Applications (WRLA). Lecture Notes in Computer Science, vol. 14953, pp. 3\u201321. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65941-6_1","DOI":"10.1007\/978-3-031-65941-6_1"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: International Conference on Rewriting Techniques and Applications (RTA). LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013). https:\/\/doi.org\/10.4230\/LIPICS.RTA.2013.81","DOI":"10.4230\/LIPICS.RTA.2013.81"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Bae, K., Meseguer, J.: Predicate abstraction of rewrite theories. In: Rewriting and Typed Lambda Calculi - Joint International Conference, (RTA-TLCA). Lecture Notes in Computer Science, vol.\u00a08560, pp. 61\u201376. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_5","DOI":"10.1007\/978-3-319-08918-8_5"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"van\u00a0der Berg, F.I., Laarman, A.: SpinS: extending LTSmin with PROMELA through SpinJa. In: International Workshop on Parallel and Distributed Methods in Verification (PDMC). Electronic Notes in Theoretical Computer Science, vol.\u00a0296, pp. 95\u2013105. Elsevier (2012). https:\/\/doi.org\/10.1016\/J.ENTCS.2013.07.007","DOI":"10.1016\/J.ENTCS.2013.07.007"},{"key":"16_CR5","unstructured":"Bevier, W.: Toward an operational semantics of PROMELA in ACL2. In: Proceedings of the Third SPIN Workshop (1997)"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Bogdanas, D., Rosu, G.: K-Java: a complete semantics of Java. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 445\u2013456. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: International Workshop on Rewriting Logic and its Applications (WRLA). Electronic Notes in Theoretical Computer Science, vol.\u00a0117, pp. 393\u2013416. Elsevier (2004). https:\/\/doi.org\/10.1016\/J.ENTCS.2004.06.019","DOI":"10.1016\/J.ENTCS.2004.06.019"},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/S10703-006-0027-9","volume":"30","author":"Y Choi","year":"2007","unstructured":"Choi, Y.: From NuSMV to SPIN: experiences with model checking flight guidance systems. Formal Methods Syst. Des. 30(3), 199\u2013216 (2007). https:\/\/doi.org\/10.1007\/S10703-006-0027-9","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR9","unstructured":"Comini, M., Gallardo, M., Villanueva, A.: A denotational semantics for PROMELA addressing arbitrary jumps. CoRR arxiv:2108.12348 (2021)"},{"issue":"1\u20132","key":"16_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0304-3975(01)00165-7","volume":"275","author":"P Degano","year":"2002","unstructured":"Degano, P., Gadducci, F., Priami, C.: A causal semantics for CCS via rewriting logic. Theor. Comput. Sci. 275(1\u20132), 259\u2013282 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00165-7","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"16_CR11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 533\u2013544. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Evrard, H., Donaldson, A.F.: Model checking futexes. In: Model Checking Software (SPIN). Lecture Notes in Computer Science, vol. 13872, pp. 41\u201358. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-32157-3_3","DOI":"10.1007\/978-3-031-32157-3_3"},{"issue":"3","key":"16_CR14","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/S00165-004-0040-Y","volume":"16","author":"M Gallardo","year":"2004","unstructured":"Gallardo, M., Merino, P., Pimentel, E.: A generalized semantics of PROMELA for abstract model checking. Formal Aspects Comput. 16(3), 166\u2013193 (2004). https:\/\/doi.org\/10.1007\/S00165-004-0040-Y","journal-title":"Formal Aspects Comput."},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: Computer Security Foundations Symposium (CSF), pp. 204\u2013217. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: Theories of Programming: The Life and Works of Tony Hoare, ACM Books, vol.\u00a039, pp. 157\u2013186. ACM\/Morgan & Claypool (2021). https:\/\/doi.org\/10.1145\/3477355.3477364","DOI":"10.1145\/3477355.3477364"},{"issue":"5","key":"16_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"de\u00a0Jonge, M., Ruys, T.C.: The SpinJa model checker. In: Model Checking Software (SPIN). Lecture Notes in Computer Science, vol.\u00a06349, pp. 124\u2013128. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16164-3_9","DOI":"10.1007\/978-3-642-16164-3_9"},{"key":"16_CR19","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2024.103097","volume":"235","author":"B Kang","year":"2024","unstructured":"Kang, B., Bae, K.: Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systems. Sci. Comput. Program. 235, 103097 (2024). https:\/\/doi.org\/10.1016\/J.SCICO.2024.103097","journal-title":"Sci. Comput. Program."},{"issue":"8","key":"16_CR20","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974). https:\/\/doi.org\/10.1145\/361082.361093","journal-title":"Commun. ACM"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Lazar, D., et al.: Executing formal semantics with the K tool. In: International Symposium on Formal Methods (FM). Lecture Notes in Computer Science, vol.\u00a07436, pp. 267\u2013271. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_23","DOI":"10.1007\/978-3-642-32759-9_23"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Maggi, P., Sisto, R.: Using SPIN to verify security properties of cryptographic protocols. In: Model Checking of Software (SPIN). Lecture Notes in Computer Science, vol.\u00a02318, pp. 187\u2013204. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46017-9_14","DOI":"10.1007\/3-540-46017-9_14"},{"issue":"1","key":"16_CR23","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theor. Comput. Sci."},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.\u00a092. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"issue":"1","key":"16_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4","journal-title":"I. Inf. Comput."},{"key":"16_CR26","unstructured":"Natarajan, V., Holzmann, G.: Outline for an operational semantics of PROMELA. In: Proceedings of the Second SPIN Workshop (1996)"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Neumann, R.: Using PROMELA in a fully verified executable LTL model checker. In: International Conference on Verified Software: Theories, Tools and Experiments (VSTTE). Lecture Notes in Computer Science, vol.\u00a08471, pp. 105\u2013114. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_7","DOI":"10.1007\/978-3-319-12154-3_7"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Park, D., Stefanescu, A., Rosu, G.: KJS: a complete formal semantics of JavaScript. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 346\u2013356. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Park, D., Zhang, Y., Rosu, G.: End-to-end formal verification of Ethereum 2.0 deposit smart contract. In: International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 12224, pp. 151\u2013164. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_8","DOI":"10.1007\/978-3-030-53288-8_8"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Rosu, G.: A formal verification tool for Ethereum VM bytecode. In: ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 912\u2013915. ACM (2018). https:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"16_CR31","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Methods Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Rosu, G.: Matching logic. Log. Methods Comput. Sci. 13(4) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(4:28)2017","DOI":"10.23638\/LMCS-13(4:28)2017"},{"issue":"6","key":"16_CR33","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/J.JLAP.2010.03.012","volume":"79","author":"G Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/J.JLAP.2010.03.012","journal-title":"J. Log. Algebraic Methods Program."},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Sharma, A.: A refinement calculus for PROMELA. In: International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 75\u201384. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/ICECCS.2013.20","DOI":"10.1109\/ICECCS.2013.20"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. In: International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR). Lecture Notes in Computer Science, vol. 10855, pp. 201\u2013217. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-94460-9_12","DOI":"10.1007\/978-3-319-94460-9_12"},{"key":"16_CR36","unstructured":"Spin Online References: PROMELA manual pages. https:\/\/spinroot.com\/spin\/Man\/promela.html. Accessed 20 Nov 2025"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Stefanescu, A., Ciob\u00e2c\u0103, \u015e., Mereuta, R., Moore, B.M., Serbanuta, T., Rosu, G.: All-path reachability logic. In: Rewriting and Typed Lambda Calculi - Joint International Conference (RTA-TLCA). Lecture Notes in Computer Science, vol.\u00a08560, pp. 425\u2013440. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_29","DOI":"10.1007\/978-3-319-08918-8_29"},{"key":"16_CR38","doi-asserted-by":"publisher","unstructured":"Stehr, M.: CINNI - a generic calculus of explicit substitutions and its application to lambda-, varsigma- and pi- calculi. In: International Workshop on Rewriting Logic and its Applications (WRLA). Electronic Notes in Theoretical Computer Science, vol.\u00a036, pp. 70\u201392. Elsevier (2000). https:\/\/doi.org\/10.1016\/S1571-0661(05)80125-2","DOI":"10.1016\/S1571-0661(05)80125-2"},{"key":"16_CR39","doi-asserted-by":"publisher","unstructured":"Thati, P., Sen, K., Mart\u00ed-Oliet, N.: An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0. In: International Workshop on Rewriting logic and Its Applications (WRLA). Electronic Notes in Theoretical Computer Science, vol.\u00a071, pp. 261\u2013281. Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(05)82539-3","DOI":"10.1016\/S1571-0661(05)82539-3"},{"issue":"1\u20132","key":"16_CR40","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/S10703-005-2254-X","volume":"27","author":"A Verdejo","year":"2005","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods Syst. Des. 27(1\u20132), 113\u2013172 (2005). https:\/\/doi.org\/10.1007\/S10703-005-2254-X","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR41","doi-asserted-by":"publisher","unstructured":"Viry, P.: Input\/output for ELAN. In: International Workshop on Rewriting Logic and its Applications (WRLA). Electronic Notes in Theoretical Computer Science, vol.\u00a04, pp. 51\u201364. Elsevier (1996). https:\/\/doi.org\/10.1016\/S1571-0661(04)00033-7","DOI":"10.1016\/S1571-0661(04)00033-7"},{"key":"16_CR42","unstructured":"Weise, C.: An incremental formal semantics for PROMELA. In: Proceedings of the Third SPIN Workshop (1997)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:51Z","timestamp":1768202511000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_16","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":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 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":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}