The rewriting logic semantics project. (English) Zbl 1111.68068

Summary: Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory’s axioms include both equations and rewrite rules provides a useful “abstraction dial” to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.


68Q55 Semantics in the theory of computing
68Q42 Grammars and rewriting systems
Full Text: DOI Link


[1] Ahrendt, W.; Roth, A.; Sasse, R., Automatic validation of transformation rules for Java verification against a rewriting semantics, (), 412-426 · Zbl 1143.68348
[2] Basin, D.; Denker, G., Maude versus Haskell: an experimental comparison in security protocol analysis, () · Zbl 0962.68056
[3] Beckert, B., A dynamic logic for the formal verification of Java card programs, (), 6-24 · Zbl 0980.68525
[4] Berry, G.; Boudol, G., The chemical abstract machine, Theoretical computer science, 96, 1, 217-248, (1992) · Zbl 0747.68013
[5] Bouhoula, A.; Jouannaud, J.-P.; Meseguer, J., Specification and proof in membership equational logic, Theoretical computer science, 236, 35-132, (2000) · Zbl 0938.68057
[6] C. Braga, Rewriting logic as a semantic framework for modular structural operational semantics, Ph.D. Thesis, Departamento de Informática, Pontificia Universidade Católica de Rio de Janeiro, Brasil, 2001
[7] Braga, C.; Meseguer, J., Modular rewriting semantics in practice, () · Zbl 1272.68168
[8] Broy, M.; Wirsing, M.; Pepper, P., On the algebraic definition of programming languages, ACM transactions on programming languages and systems, 9, 1, 54-99, (1987) · Zbl 0627.68009
[9] Bruni, R.; Meseguer, J., Generalized rewrite theories, (), 252-266 · Zbl 1039.03020
[10] Cervesato, I.; Stehr, M.-O., Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types, () · Zbl 1115.68073
[11] F. Chalub, An implementation of modular SOS in Maude, Master’s Thesis, Universidade Federal Fluminense, May 2005,http://www.ic.uff.br/ frosario/dissertation.pdf
[12] Chalub, F.; Braga, C., A modular rewriting semantics for CML, Journal of universal computer science, 10, 7, 789-807, (2004)
[13] F. Chen, G. Roşu, Rewriting logic semantics of Java 1.4, http://fsl.cs.uiuc.edu/index.php/Rewriting_Logic_Semantics_of_Java
[14] Chen, F.; Roşu, G., Certifying measurement unit safety policy, (), 304-309
[15] Chen, F.; Roşu, G.; Venkatesan, R.P., Rule-based analysis of dimensional safety, (), 197-207 · Zbl 1038.68548
[16] Clarke, E.M.; Grumberg, O.; Peled, D.A., Model checking, (2001), MIT Press
[17] 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) · Zbl 1001.68059
[18] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. Talcott, Maude 2.0 Manual, June 2003, http://maude.cs.uiuc.edu
[19] Clavel, M.; Durán, F.; Eker, S.; Meseguer, J., Building equational proving tools by reflection in rewriting logic, ()
[20] M. Clavel, M. Palomino, The ITP tool’s manual. Universidad Complutense, Madrid, April 2005, http://maude.sip.ucm.es/itp/
[21] Clavel, M.; Santa-Cruz, J., ASIP+ITP: A verification tool based on algebraic semantics, ()
[22] Clément, D.; Despeyroux, J.; Hascoet, L.; Kahn, G., Natural semantics on the computer, (), 49-89, Also, Information Processing Society of Japan, Technical Memorandum PL-86-6
[23] d’Amorim, M.; Roşu, G., An equational specification for the scheme language, Journal of universal computer science, 11, 7, 1327-1348, (2005)
[24] Eker, S.; Meseguer, J.; Sridharanarayanan, A., The maude LTL model checker, () · Zbl 1272.68243
[25] Farzan, A.; Chen, F.; Meseguer, J.; Roşu, G., Formal analysis of Java programs in javafan, (), 501-505 · Zbl 1103.68611
[26] A. Farzan, J. Meseguer, Making partial order reduction tools language-independent, in: G. Denker, C. Talcott (Eds.), Proc. 6th. Intl. Workshop on Rewriting Logic and its Applications, in: ENTCS, Elsevier, 2006 (in press) · Zbl 1236.68182
[27] Farzan, A.; Meseguer, J.; Roşu, G., Formal JVM code analysis in javafan, (), 132-147 · Zbl 1108.68382
[28] Felleisen, M.; Freidman, D.P., Control operators, the SECD machine, and the \(\lambda\)-calculus, (), 193-217
[29] A. Garrido, Program refactoring in the presence of preprocessor directives, Ph.D. Thesis, University of Illinois at Urbana-Champaign, 2005
[30] A. Garrido, J. Meseguer, R. Johnson, Algebraic semantics of the C preprocessor and correctness of its refactorings, Technical Report UIUCDCS-R-2006-2688, University of Illinois at Urbana-Champaign, February 2006
[31] Goguen, J.A.; Malcolm, G., Algebraic semantics of imperative programs, (1996), MIT Press · Zbl 0887.68066
[32] Goguen, J.A.; Parsaye-Ghomi, K., Algebraic denotational semantics using parameterized abstract modules, (), 292-309 · Zbl 0467.68014
[33] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J., Initial algebra semantics and continuous algebras, Journal of the association for computing machinery, 24, 1, 68-95, (1977) · Zbl 0359.68018
[34] Hartel, P.H., LETOS—a lightweight execution tool for operational semantics, Software: practice and experience, 29, 1379-1416, (1999)
[35] Hennessy, M., The semantics of programming languages: an elementary introduction using structural operational semantics, (1990), John Wiley & Sons · Zbl 0723.68067
[36] M. Hills, T.F. Şerbănuţă, G. Roşu, A rewrite framework for language definitions and for generation of efficient interpreters, in: Proceedings of WRLA’06, in: ENTCS, Elsevier, 2006 (in press) · Zbl 1279.68116
[37] Johnsen, E.B.; Owe, O.; Axelsen, E.W., A runtime environment for concurrent objects with asynchronous method calls, ()
[38] M. Katelman, J. Meseguer, A rewriting semantics for abel with applications to hardware/software co-design and analysis, in: G. Denker, C. Talcott (Eds.), Proceedings of WRLA’06, in: ENTCS, Elsevier, 2006 (in press) · Zbl 1279.68189
[39] Lowry, M.; Pressburger, T.; Roşu, G., Certifying domain-specific policies, (), 81-90
[40] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoretical computer science, 96, 1, 73-155, (1992) · Zbl 0758.68043
[41] Meseguer, J., Membership algebra as a logical framework for equational specification, (), 18-61 · Zbl 0903.08009
[42] Meseguer, J., Software specification and verification in rewriting logic, (), 133-193
[43] J. Meseguer, Lecture notes on program verification. CS 476, University of Illinois, Spring 2005, http://www.cs.uiuc.edu/class/fa05/cs476/
[44] Meseguer, J.; Braga, C., Modular rewriting semantics of programming languages, (), 364-378 · Zbl 1108.68401
[45] Meseguer, J.; Roşu, G., Rewriting logic semantics: from language specifications to formal analysis tools, (), 1-44 · Zbl 1126.68464
[46] J. Meseguer, G. Roşu, The rewriting logic semantics project, Technical Report UIUCDCS-R-2005-2639, University of Illinois at Urbana-Champaign, 2005. Ask authors for the complete Maude code
[47] Milner, R., Functions as processes, Mathematical structures in computer science, 2, 2, 119-141, (1992) · Zbl 0773.03012
[48] J. Moore, R. Krug, H. Liu, G. Porter, Formal models of Java at the JVM level—a survey from the ACL2 perspective, in: Proc. Workshop on Formal Techniques for Java Programs, in Association with ECOOP 2001, 2002
[49] Mosses, P.D., Unified algebras and action semantics, (), 17-35
[50] Mosses, P.D., Denotational semantics, (), (Chapter 11) · Zbl 0338.68021
[51] Mosses, P.D., Foundations of modular SOS, (), 70-80 · Zbl 0955.68075
[52] Mosses, P.D., Pragmatics of modular SOS, (), 21-40 · Zbl 1275.68086
[53] Mosses, P.D., Modular structural operational semantics, Journal of logic and algebraic programming, 60-61, 195-228, (2004) · Zbl 1072.68061
[54] Pettersson, M., ()
[55] Plotkin, G.D., A structural approach to operational semantics, Journal of logic and algebraic programming, 60-61, 17-139, (2004), Previously published as technical report DAIMI FN-19, Computer Science Department, Aarhus University, 1981 · Zbl 1082.68062
[56] G. Roşu, Programming language design and semantics classes, Department of Computer Science, University of Illinois at Urbana-Champaign. http://fsl.cs.uiuc.edu/ grosu/classes/
[57] G. Roşu, K: A Rewrite Logic Framework for Language Design, Semantics, Analysis and Implementation, Technical Report UIUCDCS-R-2005-2672, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005
[58] Roşu, G.; Venkatesan, R.P.; Whittle, J.; Leuştean, L., Certifying optimality of state estimation programs, (), 301-314 · Zbl 1278.68193
[59] R. Sasse, Taclets vs. rewriting logic—relating semantics of Java, Master’s Thesis, Fakultät für Informatik, Universität Karlsruhe, Technical Report in Computing Science No. 2005-16, Germany, May 2005, http://www.ubka.uni-karlsruhe.de/cgi-bin/psview?document=ira/2005/16
[60] R. Sasse, J. Meseguer, Java+ITP: A verification tool based on Hoare logic and algebraic semantics, in: G. Denker, C. Talcott (Eds), Proceedings of WRLA’06, in: ENTCS, Elsevier, 2006 (in press)
[61] Schmidt, D.A., Denotational semantics—A methodology for language development, (1986), Allyn and Bacon Boston, MA
[62] D. Scott, Outline of a mathematical theory of computation, in: Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems, Princeton University, 1970, pp. 169-176. Also appeared as Technical Monograph PRG 2, Oxford University, Programming Research Group
[63] Scott, D.; Strachey, C., Toward a mathematical semantics for computer languages, () · Zbl 0268.68004
[64] Stehr, M.-O.; Cervesato, I.; Reich, S., An execution environment for the MSR cryptoprotocol specification language
[65] Stehr, M.-O.; Talcott, C., PLAN in maude: specifying an active network programming language, () · Zbl 1272.68044
[66] M.-O. Stehr, C.L. Talcott, Practical techniques for language design and prototyping, in: J.L. Fiadeiro, U. Montanari, M. Wirsing (Eds.), Abstracts Collection of the Dagstuhl Seminar 05081 on Foundations of Global Computing, February 20-25, 2005, Schloss Dagstuhl, Wadern, Germany, 2005
[67] Thati, P.; Sen, K.; Martí-Oliet, N., An executable specification of asynchronous pi-calculus semantics and may testing in maude 2.0, () · Zbl 1272.68322
[68] A. Verdejo, Maude como marco semántico ejecutable, Ph.D. Thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain, 2003
[69] A. Verdejo, N. Martí-Oliet, Executable structural operational semantics in Maude, Manuscript, Dto. Sistemas Informáticos y Programación, Universidad Complutense, Madrid, August 2003
[70] Verdejo, A.; Martí-Oliet, N., Implementing CCS in maude 2, () · Zbl 1086.68552
[71] Viry, P., Equational rules for rewriting logic, Theoretical computer science, 285, 487-517, (2002) · Zbl 1001.68058
[72] Wand, M., First-order identities as a defining language, Acta informatica, 14, 337-357, (1980) · Zbl 0424.68022
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.