{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T17:34:47Z","timestamp":1762623287922,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":89,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223450"},{"type":"electronic","value":"9783540259848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25984-8_1","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T02:31:38Z","timestamp":1284172298000},"page":"1-44","source":"Crossref","is-referenced-by-count":28,"title":["Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Proceedings of WRLA 1996, September 1996. ENTCS, vol.\u00a04, Elsevier, Amsterdam (1996), http:\/\/www.elsevier.nl\/locate\/entcs\/volume4.html"},{"key":"1_CR2","unstructured":"Baker, H., Hewitt, C.: Laws for communicating parallel processes. In: Proceedings of the 1977 IFIP Congress, pp. 987\u2013992. IFIP Press (1977)"},{"key":"1_CR3","series-title":"ENTCS","volume-title":"Proc. 3rd. WRLA","author":"D. Basin","year":"2000","unstructured":"Basin, D., Denker, G.: Maude versus Haskell: an experimental comparison in security protocol analysis. In: Proc. 3rd. WRLA. ENTCS, Elsevier, Amsterdam (2000)"},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G. Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science\u00a096(1), 217\u2013248 (1992)","journal-title":"Theoretical Computer Science"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0304-3975(87)90090-9","volume":"55","author":"E. Best","year":"1989","unstructured":"Best, E., Devillers, R.: Sequential and concurrent behavior in Petri net theory. Theoretical Computer Science\u00a055, 87\u2013136 (1989)","journal-title":"Theoretical Computer Science"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","volume":"285","author":"P. Borovansk\u00fd","year":"2002","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science\u00a0285, 155\u2013185 (2002)","journal-title":"Theoretical Computer Science"},{"key":"1_CR7","first-page":"169","volume-title":"Algebraic Methods in Semantics","author":"G. Boudol","year":"1985","unstructured":"Boudol, G.: Computational semantics of term rewriting systems. In: Algebraic Methods in Semantics, pp. 169\u2013236. Cambridge University Press, Cambridge (1985)"},{"key":"1_CR8","unstructured":"Braga, C.: Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics. PhD thesis, Departamento de Inform\u00e1tica, Pontificia Universidade Cat\u00f3lica de Rio de Janeiro, Brasil (2001)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45013-0_21","volume-title":"Logic Based Program Synthesis and Transformation","author":"C. Braga","year":"2003","unstructured":"Braga, C., Haeusler, E.H., Meseguer, J., Mosses, P.D.: Mapping modular SOS to rewriting logic. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664, pp. 262\u2013277. Springer, Heidelberg (2003)"},{"key":"1_CR10","unstructured":"Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: Proc. WRLA 2004. ENTCS (2004)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Model checking programs. In: ASE 2000, pp. 3\u201312 (2000)","DOI":"10.1109\/ASE.2000.873645"},{"issue":"1","key":"1_CR12","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/9758.10501","volume":"9","author":"M. Broy","year":"1987","unstructured":"Broy, M., Wirsing, M., Pepper, P.: On the algebraic definition of programming languages. ACM Trans. on Prog. Lang. and Systems\u00a09(1), 54\u201399 (1987)","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"1_CR13","unstructured":"Bruni, R.: Tile Logic for Synchronized Rewriting of Concurrent Systems. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa (1999), Technical Report TD-1\/99, http:\/\/www.di.unipi.it\/phd\/tesi\/tesi_1999\/TD-1-99.ps.gz"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-45061-0_22","volume-title":"Automata, Languages and Programming","author":"R. Bruni","year":"2003","unstructured":"Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 252\u2013266. Springer, Heidelberg (2003)"},{"key":"1_CR15","series-title":"ENTCS","first-page":"253","volume-title":"Proceedings of WRLA 1998","author":"G. Carabetta","year":"1998","unstructured":"Carabetta, G., Degano, P., Gadducci, F.: CCS semantics via proved transition systems and rewriting logic. In: Proceedings of WRLA 1998, September 1-4. ENTCS, vol.\u00a015, pp. 253\u2013272. Elsevier, Amsterdam (1998), http:\/\/www.elsevier.nl\/locate\/entcs\/volume15.html"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-44881-0_15","volume-title":"Rewriting Techniques and Applications","author":"F. Chen","year":"2003","unstructured":"Chen, F., Ro\u015fu, G., Venkatesan, R.P.: Rule-based analysis of dimensional safety. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 197\u2013207. Springer, Heidelberg (2003)"},{"key":"1_CR17","volume-title":"Model Checking","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science\u00a0285, 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"1_CR19","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (June 2003), http:\/\/maude.cs.uiuc.edu"},{"key":"1_CR20","volume-title":"CAFE: An Industrial-Strength Algebraic Formal Method","author":"M. Clavel","year":"2000","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method, Elsevier, Amsterdam (2000), http:\/\/maude.cs.uiuc.edu"},{"key":"1_CR21","unstructured":"Cl\u00e9ment, D., Despeyroux, J., Hascoet, L., Kahn, G.: Natural semantics on the computer. In: Proceedings, France-Japan AI and CS Symposium, pp. 49\u201389. ICOT, Also, Information Processing Society of Japan, Technical Memorandum PL-86-6 (1986)"},{"issue":"1-2","key":"1_CR22","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. Theoretical Computer Science\u00a0275(1-2), 259\u2013282 (2002)","journal-title":"Theoretical Computer Science"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Montanari, U. (eds.): Selected papers of the 2nd workshop on concurrency and compositionality, March 1990. Theoretical Computer Science, vol.\u00a096(1) (1992)","DOI":"10.1016\/0304-3975(92)90179-J"},{"key":"1_CR24","series-title":"ENTCS","volume-title":"Proc. 4th. WRLA","author":"S. Eker","year":"2002","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Proc. 4th. WRLA. ENTCS, Elsevier, Amsterdam (2002)"},{"key":"1_CR25","unstructured":"Farzan, A., Chen, F., Meseguer, J., Ro\u015fu, G.: JavaFAN, http:\/\/fsl.cs.uiuc.edu\/javafan"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Cheng, F., Meseguer, J., Ro\u015fu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 501\u2013505. Springer, Heidelberg (2004)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-27815-3_14","volume-title":"Algebraic Methodology and Software Technology","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Meseguer, J., Ro\u015fu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 132\u2013147. Springer, Heidelberg (2004)"},{"key":"1_CR28","series-title":"AMAST Series","volume-title":"Cafe OBJ Report","author":"K. Futatsugi","year":"1998","unstructured":"Futatsugi, K., Diaconescu, R.: Cafe OBJ Report. AMAST Series. World Scientific, Singapore (1998)"},{"key":"1_CR29","doi-asserted-by":"crossref","first-page":"133","DOI":"10.7551\/mitpress\/5641.003.0010","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"F. Gadducci","year":"2000","unstructured":"Gadducci, F., Montanari, U.: The tile model. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 133\u2013166. MIT Press, Cambridge (2000)"},{"key":"1_CR30","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1188.001.0001","volume-title":"Algebraic Semantics of Imperative Programs","author":"J.A. Goguen","year":"1996","unstructured":"Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-10699-5_106","volume-title":"Formalization of Programming Concepts","author":"J.A. Goguen","year":"1981","unstructured":"Goguen, J.A., Parsaye-Ghomi, K.: Algebraic denotational semantics using parameterized abstract modules. In: D\u00edaz, J., Ramos, I. (eds.) Formalization of Programming Concepts. LNCS, vol.\u00a0107, pp. 292\u2013309. Springer, Heidelberg (1981)"},{"key":"1_CR32","unstructured":"Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.: Formal analysis of the remote agent before and after flight. In: The 5th NASA Langley Formal Methods Workshop (2000)"},{"issue":"8","key":"1_CR33","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K. Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M., Penix, J.: Formal Analysis of a Space Craft Controller using SPIN. IEEE Transactions on Software Engineering\u00a027(8), 749\u2013765 (2001); Previous version appeared in Proceedings of the 4th SPIN workshop (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"1_CR34","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"Software Tools for Technology Transfer"},{"key":"1_CR35","volume-title":"The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics","author":"M. Hennessy","year":"1990","unstructured":"Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. John Willey & Sons, West Sussex (1990)"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","volume-title":"Conditional and Typed Rewriting Systems","author":"C. Hintermeier","year":"1995","unstructured":"Hintermeier, C.: How to transform canonical decreasing ctrss into equivalent canonical trss. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, Springer, Heidelberg (1995)"},{"key":"1_CR37","unstructured":"Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. Technical Report NIII-R0318, Computing Science Institute, University of Nijmegen (2000)"},{"key":"1_CR38","series-title":"ENTCS","volume-title":"Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications","author":"E.B. Johnsen","year":"2004","unstructured":"Johnsen, E.B., Owe, O., Axelsen, E.W.: A runtime environment for concurrent objects with asynchronous method calls. In: Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2004)"},{"key":"1_CR39","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S0960129500000980","volume":"6","author":"C. Laneve","year":"1996","unstructured":"Laneve, C., Montanari, U.: Axiomatizing permutation equivalence. Mathematical Structures in Computer Science\u00a06, 219\u2013249 (1996)","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR40","first-page":"1","volume-title":"Rewriting logic as a logical and semantic framework. In: Handbook of Philosophical Logic","author":"N. Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Handbook of Philosophical Logic, 2nd edn., pp. 1\u201387. Kluwer Academic Publishers, Dordrecht (2002)","edition":"2"},{"issue":"1","key":"1_CR41","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 unified model of concurrency. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"1_CR42","doi-asserted-by":"crossref","first-page":"314","DOI":"10.7551\/mitpress\/2087.003.0017","volume-title":"Research Directions in Concurrent Object-Oriented Programming","author":"J. Meseguer","year":"1993","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Research Directions in Concurrent Object-Oriented Programming, pp. 314\u2013390. The MIT Press, Cambridge (1993)"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-61604-7_64","volume-title":"CONCUR \u201996: Concurrency Theory","author":"J. Meseguer","year":"1996","unstructured":"Meseguer, J.: Rewriting logic as a semantic framework for concurrency: A progress report. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 331\u2013372. Springer, Heidelberg (1996)"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"1_CR45","first-page":"133","volume-title":"Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute","author":"J. Meseguer","year":"2003","unstructured":"Meseguer, J.: Software specification and verification in rewriting logic. In: Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute, July 30 - August 11, 2002, pp. 133\u2013193. IOS Press, Amsterdam (2003)"},{"key":"1_CR46","volume-title":"Lecture notes on program verification. CS 376","author":"J. Meseguer","year":"2003","unstructured":"Meseguer, J.: Lecture notes on program verification. CS 376. University of Illinois (Fall 2003) http:\/\/www-courses.cs.uiuc.edu\/~cs376\/"},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-540-27815-3_29","volume-title":"Algebraic Methodology and Software Technology","author":"J. Meseguer","year":"2004","unstructured":"Meseguer, J., Braga, C.: Modular rewriting semantics of programming languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 364\u2013378. Springer, Heidelberg (2004)"},{"key":"1_CR48","unstructured":"Meseguer, J., Futatsugi, K., Winkler, T.: Using rewriting logic to specify, program, integrate, and reuse open concurrent systems of cooperating agents. In: Proceedings of the 1992 International Symposium on New Models for Software Architecture, November 1992, pp. 61\u2013106 (1992)"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-64299-4_27","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J., Montanari, U.: Mapping tile logic into rewriting logic. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 62\u201391. Springer, Heidelberg (1998)"},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-48320-9_29","volume-title":"CONCUR\u201999. Concurrency Theory","author":"J. Meseguer","year":"1999","unstructured":"Meseguer, J., Talcott, C.L.: A partial order event model for concurrent objects. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 415\u2013430. Springer, Heidelberg (1999)"},{"issue":"2","key":"1_CR51","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R. Milner","year":"1992","unstructured":"Milner, R.: Functions as processes. Mathematical Structures in Computer Science\u00a02(2), 119\u2013141 (1992)","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-540-39724-3_27","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Moore","year":"2003","unstructured":"Moore, J.: Inductive assertions and operational semantics. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 289\u2013303. Springer, Heidelberg (2003)"},{"key":"1_CR53","unstructured":"Moore, J., Krug, R., Liu, H., Porter, G.: Formal models of Java at the JVM level \u2013 a survey from the ACL2 perspective. In: Proc. Workshop on Formal Techniques for Java Programs, in association with ECOOP 2001 (2002)"},{"key":"1_CR54","unstructured":"Moore, J.S.: http:\/\/www.cs.utexas.edu\/users\/xli\/prob\/p4\/p4.html"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Mosses, P.D.: Modular structural operational semantics, to appear in J. Logic and Algebraic Programming (September 2003) (manuscript)","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"1_CR56","volume-title":"Handbook of Theoretical Computer Science","author":"P.D. Mosses","year":"1990","unstructured":"Mosses, P.D.: Denotational semantics. In: Handbook of Theoretical Computer Science, vol.\u00a0B, North-Holland, Amsterdam (1990)"},{"key":"1_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/3-540-48340-3_7","volume-title":"Mathematical Foundations of Computer Science 1999","author":"P.D. Mosses","year":"1999","unstructured":"Mosses, P.D.: Foundations of modular SOS. In: Kuty\u0142owski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol.\u00a01672, pp. 70\u201380. Springer, Heidelberg (1999)"},{"key":"1_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-45719-4_3","volume-title":"Algebraic Methodology and Software Technology","author":"P.D. Mosses","year":"2002","unstructured":"Mosses, P.D.: Pragmatics of modular SOS. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 21\u201340. Springer, Heidelberg (2002)"},{"key":"1_CR59","unstructured":"\u00d6lveczky, P.C.: Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic. PhD thesis, University of Bergen, Norway (2000), http:\/\/maude.csl.sri.com\/papers"},{"key":"1_CR60","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"P.C. \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science\u00a0285, 359\u2013405 (2002)","journal-title":"Theoretical Computer Science"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Park, D.Y.W., Stern, U., Sakkebaek, J.U., Dill, D.L.: Java model checking. In: ASE 2001, pp. 253\u2013256 (2000)","DOI":"10.1109\/ASE.2000.873671"},{"key":"1_CR62","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Dept., Aarhus University (1981)"},{"issue":"3-4","key":"1_CR63","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF01019459","volume":"6","author":"J.C. Reynolds","year":"1993","unstructured":"Reynolds, J.C.: The discoveries of continuations. LISP and Symbolic Computation\u00a06(3-4), 233\u2013247 (1993)","journal-title":"LISP and Symbolic Computation"},{"key":"1_CR64","unstructured":"Ro\u015fu, G.: Lecture notes on program language design. CS 322, University of Illinois at Urbana-Champaign (Fall 2003)"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-45069-6_30","volume-title":"Computer Aided Verification","author":"G. Ro\u015fu","year":"2003","unstructured":"Ro\u015fu, G., Venkatesan, R.P., Whittle, J., Leustean, L.: Certifying optimality of state estimation programs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 301\u2013314. Springer, Heidelberg (2003)"},{"key":"1_CR66","volume-title":"Proceedings, International Conference on Automated Software Engineering (ASE 2002)","author":"G. Ro\u015fu","year":"2002","unstructured":"Ro\u015fu, G., Whittle, J.: Towards certifying domain-specific properties of synthesized code. In: Proceedings, International Conference on Automated Software Engineering (ASE 2002), IEEE, Edinburgh (2002)"},{"key":"1_CR67","first-page":"169","volume-title":"Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems","author":"D. Scott","year":"1970","unstructured":"Scott, D.: Outline of a mathematical theory of computation. In: Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems, pp. 169\u2013176. Princeton University, Princeton (1970)"},{"key":"1_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-45740-2_21","volume-title":"Applications and Theory of Petri Nets 2001","author":"L.J. Steggles","year":"2001","unstructured":"Steggles, L.J.: Rewriting logic and Elan: Prototyping tools for Petri nets with time. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075, pp. 363\u2013381. Springer, Heidelberg (2001)"},{"key":"1_CR69","series-title":"ENTCS","volume-title":"Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications","author":"M.-O. Stehr","year":"2000","unstructured":"Stehr, M.-O.: CINNI \u2014 A generic calculus of explicit substitutions and its application to \u03bb-, \u03c2- and \u03c0-calculi. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2000)"},{"key":"1_CR70","volume-title":"Petri Nets for System Engineering \u2014 A Guide to Modeling, Verification, and Applications","author":"M.-O. Stehr","year":"2001","unstructured":"Stehr, M.-O.: A rewriting semantics for algebraic nets. In: Stehr, M.-O. (ed.) Petri Nets for System Engineering \u2014 A Guide to Modeling, Verification, and Applications, Springer, Heidelberg (2001)"},{"key":"1_CR71","unstructured":"Stehr, M.-O.: Programming, Specification, and Interactive Theorem Proving \u2014 Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory. Doctoral Thesis, Universit\u00e4t Hamburg, Fachbereich Informatik, Germany (2002), http:\/\/www.sub.uni-hamburg.de\/disse\/810\/"},{"key":"1_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-39993-3_16","volume-title":"From Object-Orientation to Formal Methods","author":"M.-O. Stehr","year":"2004","unstructured":"Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol.\u00a02635, pp. 334\u2013375. Springer, Heidelberg (2004)"},{"key":"1_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45541-8_9","volume-title":"Unifying Petri Nets","author":"M.-O. Stehr","year":"2001","unstructured":"Stehr, M.-O., Meseguer, J., \u00d6lveczky, P.: Rewriting logic as a unifying framework for Petri nets. In: Ehrig, H., Juh\u00e1s, G., Padberg, J., Rozenberg, G. (eds.) APN 2001. LNCS, vol.\u00a02128, pp. 250\u2013303. Springer, Heidelberg (2001)"},{"key":"1_CR74","series-title":"ENTCS","volume-title":"Proc. 4th. WRLA","author":"M.-O. Stehr","year":"2002","unstructured":"Stehr, M.-O., Talcott, C.: Plan in Maude: Specifying an active network programming language. In: Proc. 4th. WRLA. ENTCS, Elsevier, Amsterdam (2002)"},{"key":"1_CR75","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1023\/A:1010000313106","volume":"13","author":"C. Strachey","year":"2000","unstructured":"Strachey, C.: Fundamental concepts in programming languages. Higher-Order and Symbolic Computation\u00a013, 11\u201349 (2000)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"1_CR76","first-page":"154","volume-title":"Proceedings of FMOODS 1996","author":"C.L. Talcott","year":"1997","unstructured":"Talcott, C.L.: Interaction semantics for components of distributed systems. In: Proceedings of FMOODS 1996, pp. 154\u2013169. Chapman & Hall, Boca Raton (1997)"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Talcott, C.L.: Actor theories in rewriting logic. Theoretical Computer Science\u00a0285 (2002)","DOI":"10.1016\/S0304-3975(01)00365-6"},{"key":"1_CR78","series-title":"ENTCS","volume-title":"Proc. 4th. WRLA","author":"P. Thati","year":"2002","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: Proc. 4th. WRLA. ENTCS, Elsevier, Amsterdam (2002)"},{"key":"1_CR79","unstructured":"Turi, D.: Functorial Operational Semantics and its Denotational Dual. PhD thesis, Free University, Amsterdam (1996)"},{"key":"1_CR80","unstructured":"Verdejo, A.: Maude como marco sem\u00e1ntico ejecutable. PhD thesis, Facultad de Inform\u00e1tica, Universidad Complutense, Madrid, Spain (2003)"},{"key":"1_CR81","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Executable structural operational semantics in Maude. Dto. Sistemas Inform\u00e1ticos y Programaci\u00f3n, Universidad Complutense, Madrid (August 2003) (manuscript)"},{"key":"1_CR82","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Executing E-LOTOS processes in Maude. In: INT 2000, Extended Abstracts, Technical report 2000\/04, Technische Universitat Berlin, March 2000, pp. 49\u201353 (2000)"},{"key":"1_CR83","doi-asserted-by":"crossref","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Implementing CCS in Maude. In: Formal Methods For Distributed System Development. FORTE\/PSTV 2000 IFIP TC6 WG6, IFIP, vol.\u00a0183, pp. 351\u2013366 (2000)","DOI":"10.1007\/978-0-387-35533-7_22"},{"key":"1_CR84","series-title":"ENTCS","volume-title":"Proc. 4th. WRLA","author":"A. Verdejo","year":"2002","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Implementing CCS in Maude 2. In: Proc. 4th. WRLA. ENTCS, Elsevier, Amsterdam (2002)"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Viry, P.: Input\/output for ELAN. In: Proceedings of WRLA 1996 [1], September 3-6, pp. 51\u201364 (1996), http:\/\/www.elsevier.nl\/locate\/entcs\/volume4.html","DOI":"10.1016\/S1571-0661(04)00033-7"},{"issue":"3","key":"1_CR86","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1006\/jsco.1999.0288","volume":"28","author":"P. Viry","year":"1999","unstructured":"Viry, P.: Elimination of conditions. Journal of Symbolic Computation\u00a028(3), 381\u2013401 (1999)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR87","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science\u00a0285, 487\u2013517 (2002)","journal-title":"Theoretical Computer Science"},{"key":"1_CR88","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Java PathFinder - second generation of a Java model checker. In: Proceedings of Post-CAV Workshop on Advances in Verification (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"1_CR89","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/BF00286491","volume":"14","author":"M. Wand","year":"1980","unstructured":"Wand, M.: First-order identities as a defining language. Acta Informatica\u00a014, 337\u2013357 (1980)","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25984-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T18:11:01Z","timestamp":1740507061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25984-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223450","9783540259848"],"references-count":89,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25984-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}