Abstract
Rewriting logic is a simple computational logic very well suited as a semantic framework within which many different models of computation, systems and languages can be naturally modeled. It is also a flexible logical framework in which many different logical formalisms can be both represented and executed. As the title suggests, this paper does not try to give a comprehensive overview of rewriting logic. Instead, after introducing the basic concepts, it focuses on some recent research directions emphasizing: (i) extensions of the logic to model real-time systems and probabilistic systems; and (ii) some exciting application areas such as: semantics of programming languages, security, and bioinformatics.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Agha, G., Gunter, C., Greenwald, M., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DoS using probabilistic rewrite theories. In: Workshop on Foundations of Computer Security (FCS 2005) (Affiliated with LICS 2005) (2005)
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. In: 3rd Workshop on Quantitative Aspects of Programming Languages, QAPL 2005 (2005)
Ahrendt, W., Roth, A., Sasse, R.: Automatic validation of transformation rules for Java verification against a rewriting semantics (June 2005) (manuscript)
Basin, D., Clavel, M., Meseguer, J.: Reflective metalogical frameworks. ACM Transactions on Computational Logic (2004)
Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 55–80. Springer, Heidelberg (2000)
Basin, D., Denker, G.: Maude versus Haskell: An experimental comparison in security protocol analysis. In: Futatsugi, K. (ed.) [52], pp. 235–256, http://www.elsevier.nl/locate/entcs/volume36.html
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science 285, 155–185 (2002)
Braga, C.: Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics. PhD thesis, Departamento de Informática, Pontificia Universidade Católica de Rio de Janeiro, Brasil (2001)
Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: Proc. WRLA 2004. ENTCS (2004)
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. 2719, pp. 252–266. Springer, Heidelberg (2003)
Cervesato, I., Stehr, M.-O.: Representing the msr cryptoprotocol specification language in an extension of rewriting logic with dependent types. In: Degano, P. (ed.) Proc. Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Barcelona, Spain, March 27 - 28. Elsevier ENTCS (2004)
Chalub, F.: An implementation of modular SOS in maude. Master’s thesis, Universidade Federal Fluminense (May 2005), http://www.ic.uff.br/~frosario/dissertation.pdf
Chalub, F., Braga, C.: A Modular Rewriting Semantics for CML. Journal of Universal Computer Science 10(7), 789–807 (2004), http://www.jucs.org/jucs_10_7/a_modular_rewriting_semantics
Chen, F., Roşu, G., Venkatesan, R.P.: Rule-based analysis of dimensional safety. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 197–207. Springer, Heidelberg (2003)
Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, Stanford (2000)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J.: Metalevel computation in Maude. In: Kirchner, C., Kirchner, H. (eds.) [60], pp. 3–24, http://www.elsevier.nl/locate/entcs/volume15.html
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (June 2003), http://maude.cs.uiuc.edu
Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method, pp. 1–31. Elsevier, Amsterdam (2000), http://maude.cs.uiuc.edu
Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)
Clavel, M., Durán, F., Martí-Oliet, N.: Polytypic programming in Maude. In: Futatsugi, K. (ed.) [52], pp. 339–360, http://www.elsevier.nl/locate/entcs/volume36.html
Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. In: Meseguer, J. (ed.) Proceedings First International Workshop on Rewriting Logic and its Applications, WRLA 1996, Asilomar, California, September 3–6. Electronic Notes in Theoretical Computer Science, vol. 4, pp. 125–147. Elsevier, Amsterdam (1996), http://www.elsevier.nl/locate/entcs/volume4.html
Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Theoretical Computer Science 285, 245–288 (2002)
Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)
Clavel, M., Palomino, M.: The ITP tool’s manual. Universidad Complutense, Madrid (April 2005), http://maude.sip.ucm.es/itp/
Clavel, M., Santa-Cruz, J.: ASIP+ITP: A verification tool based on algebraic semantics. To appear in Proc. PROLE 2005 (2005), http://maude.sip.ucm.es/~clavel/pubs/
d’Amorim, M., Roşu, G.: An Equational Specification for the Scheme Language. In: Proceedings of the 9th Brazilian Symposium on Programming Languages, SBLP 2005 (2005) (to appear), Also Technical Report No. UIUCDCS-R-2005-2567(April 2005)
Denker, G., Meseguer, J., Talcott, C.: Rewriting semantics of meta-objects and composable distributed services. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2000)
Denker, G., Meseguer, J., Talcott, C.L.: Protocol specification and analysis in Maude. In: Heintze, N., Wing, J. (eds.) Proceedings of Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 25 (1998), http://www.cs.bell-labs.com/who/nch/fmsp/index.html
Denker, G., Meseguer, J., Talcott, C.L.: Formal specification and analysis of active networks and communication protocols: The Maude experience. In: Maughan, D., Koob, G., Saydjari, S. (eds.) Proceedings DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25–27, pp. 251–265. IEEE Computer Society Press, Los Alamitos (2000), http://schafercorp-ballston.com/discex/
Denker, G., Millen, J.: CAPSL and CIL language design: A common authentication protocol specification language and its intermediate language. Technical Report SRI-CSL-99-02, Computer Science Laboratory, SRI International (1999), http://www.csl.sri.com/~denker/pub_99.html
Denker, G., Millen, J.: CAPSL intermediate language. In: Heintze, N., Clarke, E. (eds.) Proceedings of Workshop on Formal Methods and Security Protocols, FMSP 1999, Trento, Italy (July 1999), http://www.cs.bell-labs.com/who/nch/fmsp99/program.html
Denker, G., Millen, J.: CAPSL integrated protocol environment. In: Maughan, D., Koob, G., Saydjari, S. (eds.) Proceedings DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25-27, pp. 207–222. IEEE Computer Society Press, Los Alamitos (2000), http://schafercorp-ballston.com/discex/
Denker, G., Millen, J.: The CAPSL integrated protocol environment. Technical Report SRI-CSL-2000-02, Computer Science Laboratory, SRI International (2000), http://www.csl.sri.com/~denker/pub_99.html
Durán, F.: A reflective module algebra with applications to the Maude language. Ph.D. Thesis, University of Málaga (1999)
Durán, F.: Coherence checker and completion tools for Maude specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
Durán, F.: The extensibility of Maude’s module algebra. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 422–437. Springer, Heidelberg (2000)
Durán, F.: Termination checker and Knuth-Bendix completion tools for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Proc. of ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, PEPM 2004, pp. 147–158. ACM Press, New York (2004)
Durán, F., Meseguer, J.: An extensible module algebra for Maude. In: Kirchner, Kirchner (eds.) [60], pp. 185–206., http://www.elsevier.nl/locate/entcs/volume15.html
Durán, F., Meseguer, J.: A Church-Rosser checker tool for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
Durán, F., Meseguer, J.: On parameterized theories and views in Full Maude 2.0. In: Futatsugi, K. (ed.) Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2000)
Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway logic: Symbolic analysis of biological signaling. In: Proceedings of the Pacific Symposium on Biocomputing, January 2002, pp. 400–412 (2002)
Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Talcott, C.: Pathway Logic: executable models of biological networks. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003)
Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer (2005) (submitted for publication)
Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 279–293. Springer, Heidelberg (2005)
Farzan, A., Cheng, F., Meseguer, J., Roşu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501–505. Springer, Heidelberg (2004)
Farzan, A., Meseguer, J.: Partial order reduction for rewriting semantics of programming languages. Technical Report UIUCDCS-R-2005-2598, CS Dept., University of Illinois at Urbana-Champaign (June 2005)
Farzan, A., Meseguer, J., Roşu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 132–147. Springer, Heidelberg (2004)
Futatsugi, K. (ed.): Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam (2000), http://www.elsevier.nl/locate/entcs/volume36.html
Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific, Singapore (1998)
Glynn, P.: The role of generalized semi-Markov processes in simulation output analysis (1983)
Gunter, C., Goodloe, A., Stehr, M.-O.: Formal prototyping in early stages of protocol design. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS 2005), Long Beach, California, January 10-11 (2005), To appear in the ACM Digital Library. Paper available at http://formal.cs.uiuc.edu/stehr/l3a-wits.pdf
Gutierrez-Nolasco, S., Venkatasubramanian, N., Stehr, M.-O., Talcott, C.L.: Exploring adaptability of secure group communication using formal prototyping techniques. In: Proceedings of the 3rd Workshop on Reflective and Adaptive Middleware (RM 2004), Toronto, Ontario, Canada, October 19 (2004), To appear in ACM Digital Library. Extended version available at http://formal.cs.uiuc.edu/stehr/spread_eng.html
Hendrix, J., Meseguer, J., Clavel, M.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)
Holzmann, G.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2003)
Johnsen, E.B., Owe, O., Axelsen, E.W.: A runtime environment for concurrent objects with asynchronous method calls. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2004)
Kirchner, C., Kirchner, H. (eds.): Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA 1998, Pont-à-Mousson, France, September 1–4. Electronic Notes in Theoretical Computer Science, vol. 15. Elsevier, Amsterdam (1998), http://www.elsevier.nl/locate/entcs/volume15.html
Kolch, W.: Meaningful relationships: the regulation of the Ras/Raf/MEK/ERK pathway by protein interactions. Biochem. J. 351, 289–305 (2000)
Kosiuczenko, P., Wirsing, M.: Timed rewriting logic with application to object-oriented specification. Technical report, Institut für Informatik, Universität München (1995)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic rewrite theories: Unifying models, logics and tools. Technical Report UIUCDCS-R-2003-2347, University of Illinois at Urbana-Champaign (May 2003)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: A rewriting based model of probabilistic distributed object systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 32–46. Springer, Heidelberg (2003)
Lien, E.: Formal modeling and analysis of the NORM multicast protocol in Real-Time Maude. Master’s thesis, Dept. of Linguistics, University of Oslo (2004), http://wo.uio.no/as/WebObjects/theses.woa/wo/0.3.9
Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., pp. 1–87. Kluwer Academic Publishers, Dordrecht (2002); First published as SRI Tech. Report SRI-CSL-93-05 (August 1993)
Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoretical Computer Science 285, 121–154 (2002)
Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Meseguer, J.: Rewriting logic as a semantic framework for concurrency: a progress report. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 331–372. Springer, Heidelberg (1996)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Meseguer, J.: Research directions in rewriting logic. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 – August 6. Springer, Heidelberg (1999)
Meseguer, J.: Software specification and verification in rewriting logic. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute, Marktoberdorf, Germany, July 30 – August 11, pp. 133–193. IOS Press, Amsterdam (2003)
Meseguer, J.: Localized fairness: A rewriting semantics. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 250–263. Springer, Heidelberg (2005)
Meseguer, J., Braga, C.: Modular rewriting semantics of programming languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 364–378. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. In: Proc. of SOS 2005. ENTCS, Elsevier, Amsterdam (2005) (to appear)
Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1–36. Springer, Heidelberg (2002)
Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2004)
Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program 60–61, 195–228 (2004)
Ölveczky, P., Keaton, M., Meseguer, J., Talcott, C., Zabele, S.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, p. 333. Springer, Heidelberg (2001)
Ölveczky, P., Meseguer, J.: Real-Time Maude 2.0. In: Proc. WRLA 2004. ENTCS (2004)
Ölveczky, 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
Ölveczky, P.C., Kosiuczenko, P., Wirsing, M.: An object-oriented algebraic steam-boiler control specification. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, pp. 379–402. Springer, Heidelberg (1996)
Ölveczky, P.C., Meseguer, J.: Specifying real-time systems in rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm
Ölveczky, P.C., Meseguer, J.: Real-Time Maude: a tool for simulating and analyzing real-time and hybrid systems. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2000)
Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)
Palomino, M.: A predicate abstraction tool for maude. Documentation and tool, available at http://maude.sip.ucm.es/~miguelpt/bibliography.html
Parzen, E.: Modern Probability Theory and its Applications. Wiley, Chichester (1960)
Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)
Roşu, 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. 2725, pp. 301–314. Springer, Heidelberg (2003)
Rodríguez, D.E.: Case studies in the specification and analysis of protocols in Maude. In: Futatsugi, K. (ed.) [52], pp. 257–275, http://www.elsevier.nl/locate/entcs/volume36.html
Sasse, R.: Taclets vs. rewriting logic – relating semantics of Java. Master’s thesis, Fakultät für Informatik, Universität Karlsruhe, Germany (May 2005), Technical Report in Computing Science No. 2005-16, http://www.ubka.uni-karlsruhe.de/cgi-bin/psview?document=ira/2005/16
Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: a case study of the alternating bit protocol. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 15. North Holland, Amsterdam (1998)
Stehr, M.-O., Cervesato, I., Reich, S.: An execution environment for the MSR cryptoprotocol specification language, http://formal.cs.uiuc.edu/stehr/msr.html
Stehr, M.-O., Talcott, C.: PLAN in Maude: Specifying an active network programming language. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)
Stehr, M.-O., Talcott, C.L.: Practical techniques for language design and prototyping. In: Fiadeiro, J.L., Montanari, U., Wirsing, M. (eds.) Abstracts Collection of the Dagstuhl Seminar 05081 on Foundations of Global Computing, Schloss Dagstuhl, Wadern, Germany, February 20–25 (2005)
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton (1994)
Talcott, C., Eker, S., Knapp, M., Lincoln, P., Laderoute, K.: Pathway logic modeling of protein functional domains in signal transduction. In: Proceedings of the Pacific Symposium on Biocomputing (January 2004)
Thati, P., Meseguer, J.: Complete symbolic reachability analysis using back-and-forth narrowing. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 379–394. Springer, Heidelberg (2005)
Thati, P., Sen, K., Martí-Oliet, N.: An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)
Thordvalsen, S.: Modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. Master’s thesis, Dept. of Informatics, University of Oslo (2005), http://heim.ifi.uio.no/~peterol/RealTimeMaude/OGDC/
Verdejo, A.: Maude como marco semántico ejecutable. PhD thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain (2003)
Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. Manuscript, Dto. Sistemas Informáticos y Programación, Universidad Complutense, Madrid (August. 2003)
Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude. In: Proc. FORTE/PSTV 2000. IFIP, vol. 183, pp. 351–366 (2000)
Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude 2. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)
Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meseguer, J. (2005). A Rewriting Logic Sampler. In: Van Hung, D., Wirsing, M. (eds) Theoretical Aspects of Computing – ICTAC 2005. ICTAC 2005. Lecture Notes in Computer Science, vol 3722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560647_1
Download citation
DOI: https://doi.org/10.1007/11560647_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29107-7
Online ISBN: 978-3-540-32072-2
eBook Packages: Computer ScienceComputer Science (R0)