{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:33:22Z","timestamp":1759991602980,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357046"},{"type":"electronic","value":"9783642357053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35705-3_8","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T01:49:52Z","timestamp":1357091392000},"page":"164-185","source":"Crossref","is-referenced-by-count":3,"title":["Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude"],"prefix":"10.1007","author":[{"given":"Huibiao","family":"Zhu","sequence":"first","affiliation":[]},{"given":"Peng","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"2003","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 System. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 76\u201387. Springer, Heidelberg (2003)"},{"key":"8_CR2","unstructured":"Clavel, M., Dur\u00e1n, F.F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.6) (January 2011)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C.: The semantic challenge of Verilog HDL. In: Proc. Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 136\u2013145. IEEE Computer Society Press (June 1995)","DOI":"10.1109\/LICS.1995.523251"},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1093\/comjnl\/45.1.27","volume":"45","author":"M.J.C. Gordon","year":"2002","unstructured":"Gordon, M.J.C.: Relating event and trace semantics of hardware description languages. The Computer Journal\u00a045(1), 27\u201336 (2002)","journal-title":"The Computer Journal"},{"key":"8_CR5","unstructured":"He, J., Xu, Q.: An operational semantics of a simulator algorithm. Technical Report 204, UNU\/IIST, P.O. Box 3058, Macau SAR, China (2000)"},{"key":"8_CR6","unstructured":"He, J., Zhu, H.: Formalising Verilog. In: Proc. ICECS 2000: IEEE International Conference on Electronics, Circuits and Systems, pp. 412\u2013415. IEEE Computer Society Press (December 2000)"},{"key":"8_CR7","unstructured":"Hoare, C.A.R.: Algebra of concurrent programming. In: Meeting 52 of WG 2.3 (2011)"},{"key":"8_CR8","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)"},{"key":"8_CR9","unstructured":"IEEE. IEEE Standard Hardware Description Language based on the Verilog Hardware Description Language, IEEE Standard 1364-1995. IEEE (1995)"},{"key":"8_CR10","unstructured":"IEEE. IEEE Standard Hardware Description Language based on the Verilog Hardware Description Language, IEEE Standard 1364-2001. IEEE (2001)"},{"key":"8_CR11","unstructured":"Li, Y., He, J.: Formalising Verilog: Operational semantics and bisimulation. Technical Report 217, UNU\/IIST, P.O. Box 3058, Macau SAR, China (November 2000)"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1016\/S1571-0661(04)00040-4","volume":"4","author":"N. Mart\u00ed-Oliet","year":"1996","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. Electronic Notes in Theoretical Computer Science\u00a04, 190\u2013225 (1996)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2","key":"8_CR13","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(01)00357-7","volume":"285","author":"N. Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic: Roadmap and bibliography. Theoretical Computer Science\u00a0285(2), 121\u2013154 (2002)","journal-title":"Theoretical Computer Science"},{"key":"8_CR14","unstructured":"Meseguer, J.: Twenty years of rewriting logic. Journal of Logic and Algebraic Programming (to appear)"},{"key":"8_CR15","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall International Series in Computer Science (1990)"},{"key":"8_CR16","unstructured":"Milner, R.: Communication and Mobile System: \u03c0-calculus. Cambridge University Press (1999)"},{"key":"8_CR17","unstructured":"Nissanke, N.: Realtime Systems. Prentice Hall International Series in Computer Science (1997)"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/S1571-0661(05)82540-X","volume":"71","author":"A. Verdejo","year":"2002","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Implementing ccs in maude 2. Electronic Notes in Theoretical Computer Science\u00a071, 282\u2013300 (2002)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"5","key":"8_CR19","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters\u00a040(5), 269\u2013276 (1991)","journal-title":"Information Processing Letters"},{"key":"8_CR20","unstructured":"Zhu, H., Bowen, J.P., He, J.: Deriving operational semantics from denotational semantics for Verilog. In: Proc. APSEC 2001: 8th Asia-Pacific Software Engineering Conference, pp. 177\u2013184. IEEE Computer Society Press (December 2001)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/3-540-44798-9_34","volume-title":"Correct Hardware Design and Verification Methods","author":"H. Zhu","year":"2001","unstructured":"Zhu, H., Bowen, J.P., He, J.: From Operational Semantics to Denotational Semantics for Verilog. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 449\u2013464. Springer, Heidelberg (2001)"},{"key":"8_CR22","unstructured":"Zhu, H., He, J.: A semantics of Verilog using Duration Calculus. In: Proc. International Conference on Software: Theory and Practice, pp. 421\u2013432 (August 2000)"},{"issue":"4","key":"8_CR23","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s11334-008-0069-9","volume":"4","author":"H. Zhu","year":"2008","unstructured":"Zhu, H., He, J., Bowen, J.P.: From algebraic semantics to denotational semantics for verilog. Innovations in Systems and Software Engineering: A NASA Journal\u00a04(4), 341\u2013360 (2008)","journal-title":"Innovations in Systems and Software Engineering: A NASA Journal"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35705-3_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T15:33:13Z","timestamp":1745940793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35705-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642357046","9783642357053"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35705-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}