{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T22:59:22Z","timestamp":1783465162879,"version":"3.55.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T00:00:00Z","timestamp":1740960000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Key Research and Development Program of China","award":["2022YFB3305102"],"award-info":[{"award-number":["2022YFB3305102"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62032024"],"award-info":[{"award-number":["62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cDigital Silk Road\u201d Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]},{"name":"Shanghai Trusted Industry Internet Software Collaborative Innovation Center"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational semantics for MDESL. This article investigates the soundness and completeness of the operational semantics for MDESL based on the denotational semantics. We introduce the concepts of transitional condition and phase semantics for each transition to show the relationship between a transition and variables in the denotational model. Then, we give the definition for the soundness and completeness of the operational semantics for MDESL. Based on our definition of the operational semantics of MDESL, we investigate the detailed theoretical proof for the soundness and completeness. Finally, a practical approach complements the theoretical one. We apply the proof assistant Coq to verify the soundness and completeness of the operational semantics for MDESL. Our research demonstrates the consistency between operational and denotational semantics for MDESL through theoretical and practical approaches.<\/jats:p>","DOI":"10.1145\/3696432","type":"journal-article","created":{"date-parts":[[2024,9,25]],"date-time":"2024-09-25T20:21:41Z","timestamp":1727295701000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESL"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-3613-3202","authenticated-orcid":false,"given":"Hongyan","family":"Zhao","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0054-1398","authenticated-orcid":false,"given":"Feng","family":"Sheng","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8608-9948","authenticated-orcid":false,"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8748-6140","authenticated-orcid":false,"given":"Jonathan","family":"Bowen","sequence":"additional","affiliation":[{"name":"School of Engineering, London South Bank University, London United Kingdom of Great Britain and Northern Ireland"},{"name":"Museophile Limited, Oxford United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,3,3]]},"reference":[{"key":"e_1_3_3_2_2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2013","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer Science & Business Media, New York."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_6"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30729-4_14"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35705-3_5"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1002\/sec.546"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_6"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0253-4"},{"key":"e_1_3_3_9_2","unstructured":"Adam Chlipala. 2008. Certified Programming with Dependent Types. Retrieved from http:\/\/adam.chlipala.net\/cpdt"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00546-3"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102510"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14806-9_2"},{"key":"e_1_3_3_14_2","article-title":"Isabelle\/UTP: Mechanised theory engineering for unifying theories of programming","author":"Foster Simon David","year":"2019","unstructured":"Simon David Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Fernando De Oliveira Salazar Ribeiro, and Burkhart Wolff. 2019. Isabelle\/UTP: Mechanised theory engineering for unifying theories of programming. Arch. Formal Proofs (2019).","journal-title":"Arch. Formal Proofs"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026928"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90219-Y"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0255(99)00015-8"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.009"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.034"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_28"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_17"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_3_3_24_2","volume-title":"Unifying Theories of Programming","author":"Hoare C. A. R.","year":"1998","unstructured":"C. A. R. Hoare and Jifeng He. 1998. Unifying Theories of Programming. Prentice Hall International Series in Computer Science."},{"key":"e_1_3_3_25_2","article-title":"The coq proof assistant a tutorial","volume":"178","author":"Huet G\u00e9rard","year":"1997","unstructured":"G\u00e9rard Huet, Gilles Kahn, and Christine Paulin-Mohring. 1997. The coq proof assistant a tutorial. Rapport Techn. 178 (1997).","journal-title":"Rapport Techn."},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2001.93352"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-019-09226-1"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.08.047"},{"key":"e_1_3_3_31_2","unstructured":"Benjamin C. Pierce Chris Casinghino Marco Gaboardi Michael Greenberg C\u0103t\u0103lin Hri\u0163cu Vilhelm Sj\u00f6berg and Brent Yorgey. 2010. Software Foundations. Retrieved from http:\/\/www.cis.upenn.edu\/bcpierce\/sf\/current\/index.html"},{"issue":"0","key":"e_1_3_3_32_2","first-page":"17","article-title":"A structural approach to operational semantics","volume":"60","author":"Plotkin Gordon D.","year":"2004","unstructured":"Gordon D. Plotkin. 2004. A structural approach to operational semantics. J. Logic Algebr. Program. 60\u201361, 0 (2004), 17\u2013139.","journal-title":"J. Logic Algebr. Program."},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3295699"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00513-4"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_34"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0453-7"},{"key":"e_1_3_3_37_2","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"Stoy Joseph E.","year":"1977","unstructured":"Joseph E. Stoy. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press."},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-013-3908-2"},{"key":"e_1_3_3_41_2","unstructured":"Hongyan Zhao. 2024. Soundness and Completeness of the Operational Semantics of MDESL. Retrieved from https:\/\/github.com\/Hongyan-Zhao\/Soundness_and_Completeness_of_the_Operational_Semantics_of_MDESL"},{"key":"e_1_3_3_42_2","volume-title":"Linking the Semantics of a Multithreaded Discrete Event Simulation Language","author":"Zhu Huibiao","year":"2005","unstructured":"Huibiao Zhu. 2005. Linking the Semantics of a Multithreaded Discrete Event Simulation Language. Ph.D. Dissertation. London South Bank University."},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2001.991475"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0069-9"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/2070618.2070635"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-010-0134-z"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0309-8"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEW.2006.22"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-009-0100-9"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.06.003"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696432","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696432","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:10:13Z","timestamp":1750295413000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696432"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,3]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3696432"],"URL":"https:\/\/doi.org\/10.1145\/3696432","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,3]]},"assertion":[{"value":"2024-02-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}