×

Programming and symbolic computation in Maude. (English) Zbl 1494.68109

Summary: Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude’s strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper.

MSC:

68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Agha, G. A.; Meseguer, J.; Sen, K., PMaude: rewrite-based specification language for probabilistic object systems, (Cerone, A.; Wiklicky, H., Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 205, Edinburgh, UK, April 2-3, 2005 (2006), Elsevier), 213-239
[2] Alpuente, M.; Ballis, D.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., \( \text{ACUOS}^2\): a high-performance system for modular ACU generalization with subtyping and inheritance, (Calimeri, F.; Leone, N.; Manna, M., Logics in Artificial Intelligence - Proceedings of the 16th European Conference. Logics in Artificial Intelligence - Proceedings of the 16th European Conference, JELIA 2019, Rende, Italy, May 7-11, 2019 (2019), Springer), 171-181 · Zbl 1525.68195
[3] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Partial evaluation of order-sorted equational programs modulo axioms, (Hermenegildo, M. V.; López-García, P., Logic-Based Program Synthesis and Transformation - 26th International Symposium. Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers (2017)), 3-20 · Zbl 1485.68050
[4] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Homeomorphic embedding modulo combinations of associativity and commutativity axioms, (Mesnard, F.; Stuckey, P. J., Logic-Based Program Synthesis and Transformation - 28th International Symposium. Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018 (2019), Springer), 38-55, Revised Selected Papers · Zbl 1524.68068
[5] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., A partial evaluation framework for order-sorted equational programs modulo axioms, J. Log. Algebraic Methods Program., 110 (2020) · Zbl 1494.68048
[6] Alpuente, M.; Escobar, S.; Espert, J.; Meseguer, J., A modular order-sorted equational generalization algorithm, Inf. Comput., 235, 98-136 (2014) · Zbl 1314.68169
[7] Bae, K.; Escobar, S.; Meseguer, J., Abstract logical model checking of infinite-state systems using narrowing, (van Raamsdonk, F., 24th International Conference on Rewriting Techniques and Applications. 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands (2013), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 81-96 · Zbl 1356.68140
[8] Bae, K.; Meseguer, J., Infinite-state model checking of LTLR formulas using narrowing, (Escobar, S., Rewriting Logic and Its Applications - 10th International Workshop. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers (2014), Springer), 113-129 · Zbl 1366.68162
[9] K. Bae, J. Meseguer, Predicate abstraction of rewrite theories, in: [36], 2014, pp. 61-76. · Zbl 1416.68118
[10] Bae, K.; Meseguer, J., Model checking linear temporal logic of rewriting formulas under localized fairness, Sci. Comput. Program., 99, 193-234 (2015)
[11] Bae, K.; Meseguer, J.; Ölveczky, P. C., Formal patterns for multirate distributed real-time systems, Sci. Comput. Program., 91, 3-44 (2014)
[12] Barrett, C.; Barbosa, H.; Brain, M.; Ibeling, D.; King, T.; Meng, P.; Niemetz, A.; Nötzli, A.; Preiner, M.; Reynolds, A.; Tinelli, C., CVC4 at the SMT competition 2018, CoRR (2018), abs/1806.08775
[13] Bergstra, J.; Tucker, J., Characterization of computable data types by means of a finite equational specification method, (de Bakker, J. W.; van Leeuwen, J., Automata, Languages and Programming, Seventh Colloquium. Automata, Languages and Programming, Seventh Colloquium, Lecture Notes in Computer Science, vol. 81 (1980), Springer-Verlag), 76-90 · Zbl 0449.68003
[14] Bobba, R.; Grov, J.; Gupta, I.; Liu, S.; Meseguer, J.; Ölveczky, P.; Skeirik, S., Design, formal modeling, and validation of cloud storage systems using Maude, (Campbell, R. H.; Kamhoua, C. A.; Kwiat, K. A., Assured Cloud Computing (2018), J. Wiley), 10-48, chapter 2
[15] P. Borovanský, C. Kirchner, H. Kirchner, P.E. Moreau, C. Ringeissen, An overview of ELAN, in: [77], 1998, pp. 55-70. · Zbl 0917.68022
[16] Bouhoula, A.; Jouannaud, J. P.; Meseguer, J., Specification and proof in membership equational logic, Theor. Comput. Sci., 236, 35-132 (2000) · Zbl 0938.68057
[17] Braga, C.; Verdejo, A., Modular structural operational semantics with strategies, (van Glabbeek, R.; Mosses, P. D., Proceedings of the Third Workshop on Structural Operational Semantics. Proceedings of the Third Workshop on Structural Operational Semantics, SOS 2006, Bonn, Germany, August 26, 2006 (2007), Elsevier), 3-17 · Zbl 1277.68114
[18] Bravenboer, M.; Kalleberg, K. T.; Vermaas, R.; Visser, E., Stratego/xt 0.17. A language and toolset for program transformation, Sci. Comput. Program., 72, 52-70 (2008)
[19] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 386-414 (2006) · Zbl 1097.68051
[20] Caballero, R.; López-Fraguas, F. J., A functional-logic perspective on parsing, (Middeldorp, A.; Sato, T., Functional and Logic Programming, Proceedings of the 4th Fuji International Symposium. Functional and Logic Programming, Proceedings of the 4th Fuji International Symposium, FLOPS’99, Tsukuba, Japan, November 11-13, 1999 (1999), Springer), 85-99 · Zbl 0988.68524
[21] Chen, S.; Meseguer, J.; Sasse, R.; Wang, H. J.; Wang, Y. M., A systematic approach to uncover security flaws in GUI logic, (2007 IEEE Symposium on Security and Privacy. 2007 IEEE Symposium on Security and Privacy, S&P 2007, 20-23 May 2007, Oakland, California, USA (2007), IEEE Computer Society), 71-85
[22] Cholewa, A.; Meseguer, J.; Escobar, S., Variants of Variants and the Finite Variant Property (2014), CS Dept. University of Illinois at Urbana-Champaign, Technical Report
[23] Ciobâcă, S.; Lucanu, D., A coinductive approach to proving reachability properties in logically constrained term rewriting systems, (Galmiche, D.; Schulz, S.; Sebastiani, R., Automated Reasoning - Proceedings of the 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference. Automated Reasoning - Proceedings of the 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018 (2018), Springer), 295-311 · Zbl 1511.68132
[24] Clavel, M.; Durán, F.; Eker, S.; Escobar, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Rubio, R.; Talcott, C., Maude Manual (Version 3.0) (2019), SRI International - University of Illinois at Urbana-Champaign
[25] Clavel, M.; Durán, F.; Eker, S.; Escobar, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., Unification and narrowing in Maude 2.4, (Treinen, R., Rewriting Techniques and Applications, Proceedings of the 20th International Conference. Rewriting Techniques and Applications, Proceedings of the 20th International Conference, RTA 2009, Brasília, Brazil, June 29-July 1, 2009 (2009), Springer), 380-390
[26] M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, C.L. Talcott, Two decades of Maude, in: [86], 2015, pp. 232-254. · Zbl 1321.68007
[27] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J., Maude: specification and programming in rewriting logic, Theor. Comput. Sci., 285, 187-243 (2002) · Zbl 1001.68059
[28] Clavel, M.; Durán, F.; Eker, S.; Meseguer, J.; Lincoln, P.; Martí-Oliet, N.; Talcott, C., All About Maude - A High-Performance Logical Framework, Lecture Notes in Computer Science, vol. 4350 (2007), Springer · Zbl 1115.68046
[29] Clavel, M.; Eker, S.; Lincoln, P.; Meseguer, J., Principles of Maude, (Meseguer, J., Proceedings of the First International Workshop on Rewriting Logic and its Applications. Proceedings of the First International Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3-6, 1996 (1996), Elsevier), 65-89 · Zbl 0912.68095
[30] Clavel, M.; Meseguer, J., Reflection in conditional rewriting logic, Theor. Comput. Sci., 285, 245-288 (2002) · Zbl 1001.68060
[31] Clavel, M.; Meseguer, J.; Palomino, M., Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Theor. Comput. Sci., 373, 70-91 (2007) · Zbl 1111.03034
[32] Clavel, M.; Palomino, M., The ITP Tool’s Manual (2005), Universidad Complutense de Madrid
[33] Colmerauer, A.; Kanoui, H.; van Caneghem, M., Étude et Réalisation d’un Système Prolog (1979), Groupe d’Intelligence Artificielle, U.E.R. de Luminy, Université d’Aix-Marseille II, Technical Report
[34] Comon-Lundh, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Giesl, J., Term Rewriting and Applications, Proceedings of the 16th International Conference. Term Rewriting and Applications, Proceedings of the 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005 (2005), Springer), 294-307 · Zbl 1078.68059
[35] Dershowitz, N.; Jouannaud, J. P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), North-Holland), 243-320 · Zbl 0900.68283
[36] (Dowek, G., Rewriting and Typed Lambda Calculi - Proceedings of the Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic. Rewriting and Typed Lambda Calculi - Proceedings of the Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Rewriting and Typed Lambda Calculi - Proceedings of the Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic. Rewriting and Typed Lambda Calculi - Proceedings of the Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Lecture Notes in Computer Science, vol. 8560 (2014), Springer) · Zbl 1291.68017
[37] Dreier, J.; Duménil, C.; Kremer, S.; Sasse, R., Beyond subterm-convergent equational theories in automated verification of stateful protocols, (Maffei, M.; Ryan, M., Principles of Security and Trust - Proceedings of the 6th International Conference. Principles of Security and Trust - Proceedings of the 6th International Conference, POST 2017, Uppsala, Sweden, April 22-29, 2017 (2017), Springer), 117-140 · Zbl 1444.68040
[38] Durán, F., The extensibility of Maude’s module algebra, (Rus, T., Algebraic Methodology and Software Technology, Proceedings of the 8th International Conference. Algebraic Methodology and Software Technology, Proceedings of the 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 20-27, 2000 (2000), Springer), 422-437 · Zbl 0983.68522
[39] Durán, F.; Eker, S.; Escobar, S.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., Built-in variant generation and unification, and their applications in Maude 2.7, (Olivetti, N.; Tiwari, A., Automated Reasoning - Proceedings of the 8th International Joint Conference. Automated Reasoning - Proceedings of the 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016 (2016), Springer), 183-192 · Zbl 1475.68046
[40] F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, C.L. Talcott, Associative unification and symbolic reasoning modulo associativity in Maude, in: [121], 2018, pp. 98-114. · Zbl 1517.68158
[41] Durán, F.; Eker, S.; Escobar, S.; Meseguer, J.; Talcott, C. L., Variants, unification, narrowing, and symbolic reachability in Maude 2.6, (Schmidt-Schauß, M., Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30-June 1, 2011, Novi Sad, Serbia (2011), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 31-40 · Zbl 1236.68180
[42] Durán, F.; Eker, S.; Lincoln, P.; Meseguer, J., Principles of Mobile Maude, (Kotz, D.; Mattern, F., Agent Systems, Mobile Agents, and Applications, Proceedings of the Second International Symposium on Agent Systems and Applications and Fourth International Symposium on Mobile Agents. Agent Systems, Mobile Agents, and Applications, Proceedings of the Second International Symposium on Agent Systems and Applications and Fourth International Symposium on Mobile Agents, ASA/MA 2000, Zürch, Switzerland, September 13-15, 2000 (2000), Springer), 73-85
[43] Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 59-88 (2008) · Zbl 1192.68154
[44] F. Durán, J. Meseguer, An extensible module algebra for Maude, in: [77], 1998, pp. 174-195. · Zbl 0919.68076
[45] Durán, F.; Meseguer, J., Structured theories and institutions, Theor. Comput. Sci., 309, 357-380 (2003) · Zbl 1070.68090
[46] Durán, F.; Meseguer, J., Maude’s module algebra, Sci. Comput. Program., 66, 125-153 (2007) · Zbl 1116.68047
[47] Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Log. Algebraic Program., 81, 816-850 (2012) · Zbl 1272.03139
[48] F. Durán, P.C. Ölveczky, A guide to extending Full Maude illustrated with the implementation of Real-Time Maude, in: [116], 2009, pp. 83-102.
[49] Durán, F.; Riesco, A.; Verdejo, A., A distributed implementation of Mobile Maude, (Denker, G.; Talcott, C., Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications. Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006 (2007), Elsevier), 113-131
[50] Durán, F.; Rocha, C.; Álvarez, J. M., Tool interoperability in the Maude Formal Environment, (Corradini, A.; Klin, B.; Cîrstea, C., Algebra and Coalgebra in Computer Science - Proceedings of the 4th International Conference. Algebra and Coalgebra in Computer Science - Proceedings of the 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011 (2011), Springer), 400-406
[51] Durán, F.; Rocha, C.; Meseguer, J., Ground confluence of order-sorted conditional specifications modulo axioms, J. Log. Algebraic Methods Program., 111 (2020) · Zbl 1498.68073
[52] Dutertre, B., Yices 2.2, (Biere, A.; Bloem, R., Computer Aided Verification - Proceedings of the 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic. Computer Aided Verification - Proceedings of the 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014 (2014), Springer), 737-744
[53] Eker, S., Fast sort computations for order-sorted matching and unification, (Agha, G.; Danvy, O.; Meseguer, J., Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday (2011), Springer), 299-314
[54] Eker, S.; Knapp, M.; Laderoute, K.; Lincoln, P.; Meseguer, J.; Sonmez, K., Pathway logic: symbolic analysis of biological signaling, (Altman, R. B.; Dunker, A. K.; Hunter, L.; Klein, T. E., Proceedings of the 7th Pacific Symposium on Biocomputing. Proceedings of the 7th Pacific Symposium on Biocomputing, PSB 2002, Lihue, Hawaii, USA, January 3-7, 2002 (2002)), 400-412
[55] Eker, S.; Martí-Oliet, N.; Meseguer, J.; Verdejo, A., Deduction, strategies, and rewriting, (Archer, M.; de la Tour, T. B.; Muñoz, C., Proceedings of the 6th International Workshop on Strategies in Automated Deduction. Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, August 16, 2006 (2007), Elsevier), 3-25 · Zbl 1277.68241
[56] Escobar, S., Functional logic programming in Maude, (Iida, S.; Meseguer, J.; Ogata, K., Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi (2014), Springer), 315-336 · Zbl 1407.68081
[57] S. Escobar, Multi-paradigm programming in Maude, in: [121], 2018, pp. 26-44.
[58] Escobar, S.; Meadows, C.; Meseguer, J., Maude-NPA: cryptographic protocol analysis modulo equational properties, (Aldini, A.; Barthe, G.; Gorrieri, R., Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures (2009), Springer), 1-50 · Zbl 1252.94061
[59] Escobar, S.; Meadows, C.; Meseguer, J.; Santiago, S., State space reduction in the Maude-NRL protocol analyzer, Inf. Comput., 238, 157-186 (2014) · Zbl 1360.94307
[60] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Log. Algebraic Program., 81, 898-928 (2012) · Zbl 1291.68217
[61] (Fioravanti, F.; Gallagher, J. P., Logic-Based Program Synthesis and Transformation - 27th International Symposium. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers. Logic-Based Program Synthesis and Transformation - 27th International Symposium. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers, Lecture Notes in Computer Science, vol. 10855 (2018), Springer) · Zbl 1392.68017
[62] H. Garavel, M. Tabikh, I. Arrada, Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages – the 4th rewrite engines competition, in: [121], 2018, pp. 1-25.
[63] Goguen, J.; Burstall, R., Institutions: abstract model theory for specification and programming, J. ACM, 39, 95-146 (1992) · Zbl 0799.68134
[64] Goguen, J.; Meseguer, J., Equality, types, modules and (why not?) generics for logic programming, J. Log. Program., 1, 179-210 (1984) · Zbl 0575.68091
[65] Goguen, J.; Meseguer, J., Eqlog: equality, types, and generic modules for logic programming, (DeGroot, D.; Lindstrom, G., Logic Programming: Functions, Relations and Equations (1986), Prentice-Hall), 295-363 · Zbl 0588.68005
[66] Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056
[67] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J. P., Introducing OBJ, (Software Engineering with OBJ: Algebraic Specification in Action (2000), Kluwer), 3-167
[68] González-Burgueño, A.; Aparicio-Sánchez, D.; Escobar, S.; Meadows, C. A.; Meseguer, J., Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA, (Barthe, G.; Sutcliffe, G.; Veanes, M., LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018 (2018), EasyChair), 400-417
[69] R. Gutiérrez, J. Meseguer, Variant-based decidable satisfiability in initial algebras with predicates, in: [61], 2018, pp. 306-322. · Zbl 1508.68060
[70] Gutiérrez, R.; Meseguer, J.; Rocha, C., Order-sorted equality enrichments modulo axioms, Sci. Comput. Program., 99, 235-261 (2015)
[71] Hendrix, J.; Meseguer, J., Order-sorted equational unification revisited, (Kniesel, G.; Pinto, J. S., Proceedings of the Ninth International Workshop on Rule-Based Programming. Proceedings of the Ninth International Workshop on Rule-Based Programming, RULE 2008, Hagenberg Castle, Austria, June 18, 2008 (2008), Elsevier), 37-50 · Zbl 1291.68220
[72] Hidalgo-Herrero, M.; Verdejo, A.; Ortega-Mallén, Y., Using Maude and its strategies for defining a framework for analyzing Eden semantics, (Antoy, S., Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming. Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2006, Seattle, WA, USA, August 11, 2006 (2007), Elsevier), 119-137 · Zbl 1277.68104
[73] Horn, A., On sentences which are true of direct unions of algebras, J. Symb. Log., 16, 14-21 (1951) · Zbl 0043.24801
[74] Jouannaud, J. P.; Kirchner, C.; Kirchner, H., Incremental construction of unification algorithms in equational theories, (Díaz, J., Automata, Languages and Programming, Proceedings of the 10th Colloquium. Automata, Languages and Programming, Proceedings of the 10th Colloquium, Barcelona, Spain, July 18-22, 1983, (1983), Springer), 361-373 · Zbl 0516.68067
[75] Katelman, M.; Keller, S.; Meseguer, J., Rewriting semantics of production rule sets, J. Log. Algebraic Program., 81, 929-956 (2012) · Zbl 1279.68188
[76] Katelman, M.; Meseguer, J.; Hou, J. C., Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking, (Barthe, G.; de Boer, F. S., Formal Methods for Open Object-Based Distributed Systems, Proceedings of the 10th IFIP WG 6.1 International Conference. Formal Methods for Open Object-Based Distributed Systems, Proceedings of the 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, (2008), Springer), 150-169
[77] (Kirchner, C.; Kirchner, H., Proceedings of the Second International Workshop on Rewriting Logic and its Applications. Proceedings of the Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-à-Mousson, France, September 1-4, 1998. Proceedings of the Second International Workshop on Rewriting Logic and its Applications. Proceedings of the Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-à-Mousson, France, September 1-4, 1998, Electronic Notes in Theoretical Computer Science, vol. 15 (1998), Elsevier) · Zbl 0903.00070
[78] Kowalski, R. A., Algorithm = logic + control, Commun. ACM, 22, 424-436 (1979) · Zbl 0404.68010
[79] Liu, S.; Ölveczky, P. C.; Meseguer, J., Modeling and analyzing mobile ad hoc networks in Real-Time Maude, J. Log. Algebraic Methods Program. (2015)
[80] Lucanu, D.; Rusu, V.; Arusoaie, A., A generic framework for symbolic execution: a coinductive approach, J. Symb. Comput., 80, 125-163 (2017) · Zbl 1356.68044
[81] D. Lucanu, V. Rusu, A. Arusoaie, D. Nowak, Verifying reachability-logic properties on rewriting-logic specifications, in: [86], 2015, pp. 451-474. · Zbl 1321.68359
[82] Lucas, S.; Meseguer, J., Normal forms and normal theories in conditional rewriting, J. Log. Algebraic Methods Program., 85, 67-97 (2016) · Zbl 1356.68124
[83] Martí-Oliet, N.; Meseguer, J., Rewriting logic as a logical and semantic framework, (Gabbay, D.; Guenthner, F., Handbook of Philosophical Logic (2002), Kluwer Academic Publishers), 1-87, First Published as SRI Tech. Report SRI-CSL-93-05, August 1993
[84] Martí-Oliet, N.; Meseguer, J.; Verdejo, A., Towards a strategy language for Maude, (Martí-Oliet, N., Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications. Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004 (2004), Elsevier), 417-441
[85] N. Martí-Oliet, J. Meseguer, A. Verdejo, A rewriting semantics for Maude strategies, in: [116], 2009, pp. 227-247. · Zbl 1347.68199
[86] (Martí-Oliet, N.; Ölveczky, P. C.; Talcott, C. L., Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday. Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 9200 (2015), Springer) · Zbl 1319.68011
[87] Martí-Oliet, N.; Palomino, M.; Verdejo, A., Strategies and simulations in a semantic framework, J. Algorithms, 62, 95-116 (2007) · Zbl 1131.68059
[88] Meier, S.; Schmidt, B.; Cremers, C.; Basin, D. A., The TAMARIN prover for the symbolic analysis of security protocols, (Sharygina, N.; Veith, H., Computer Aided Verification - Proceedings of the 25th International Conference. Computer Aided Verification - Proceedings of the 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013 (2013), Springer), 696-701
[89] Meseguer, J., General logics, (Ebbinghaus, H.; Fernandez-Prida, J.; Garrido, M.; Lascar, D.; Rodríguez Artalejo, M., Logic Colloquium’87, Proceedings of the Colloquium held in Granada. Logic Colloquium’87, Proceedings of the Colloquium held in Granada, Spain, July 20-25, 1987 (1989), North-Holland), 275-329 · Zbl 0691.03001
[90] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 73-155 (1992) · Zbl 0758.68043
[91] Meseguer, J., Multiparadigm logic programming, (Kirchner, H.; Levi, G., Algebraic and Logic Programming, Proceedings of the Third International Conference. Algebraic and Logic Programming, Proceedings of the Third International Conference, Volterra, Italy, September 2-4, 1992 (1992), Springer), 158-200 · Zbl 0856.68013
[92] Meseguer, J., A logical theory of concurrent objects and its realization in the Maude language, (Agha, G.; Wegner, P.; Yonezawa, A., Research Directions in Concurrent Object-Oriented Programming (1993), MIT Press), 314-390
[93] Meseguer, J., Solving the inheritance anomaly in concurrent object-oriented programming, (Nierstrasz, O., ECOOP’93 - Object-Oriented Programming, Proceedings of the 7th European Conference. ECOOP’93 - Object-Oriented Programming, Proceedings of the 7th European Conference, Kaiserslautern, Germany, July 26-30, 1993 (1993), Springer), 220-246
[94] Meseguer, J., Rewriting logic as a semantic framework for concurrency: a progress report, (Montanari, U.; Sassone, V., CONCUR ’96, Concurrency Theory, Proceedings of the 7th International Conference. CONCUR ’96, Concurrency Theory, Proceedings of the 7th International Conference, Pisa, Italy, August 26-29, 1996 (1996), Springer), 331-372 · Zbl 1514.68175
[95] Meseguer, J., Membership algebra as a logical framework for equational specification, (Parisi-Presicce, F., Recent Trends in Algebraic Development Techniques, 12th International Workshop. Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3-7, 1997, Selected Papers (1997), Springer), 18-61 · Zbl 0903.08009
[96] Meseguer, J., The temporal logic of rewriting: a gentle introduction, (Degano, P.; Nicola, R. D.; Meseguer, J., Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday (2008), Springer), 354-382 · Zbl 1143.68459
[97] Meseguer, J., Order-sorted parameterization and induction, (Palsberg, J., Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (2009), Springer), 43-80 · Zbl 1253.68215
[98] Meseguer, J., Twenty years of rewriting logic, J. Log. Algebraic Program., 81, 721-781 (2012) · Zbl 1267.03043
[99] Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080
[100] J. Meseguer, Generalized rewrite theories and coherence completion, in: [121], 2018, pp. 164-183. · Zbl 1517.68166
[101] Meseguer, J., Symbolic reasoning methods in rewriting logic and Maude, (Moss, L. S.; de Queiroz, R. J.G. B.; Martínez, M., Logic, Language, Information, and Computation - Proceedings of the 25th International Workshop. Logic, Language, Information, and Computation - Proceedings of the 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018 (2018), Springer), 25-60 · Zbl 1509.68121
[102] Meseguer, J., Variant-based satisfiability in initial algebras, Sci. Comput. Program., 154, 3-41 (2018) · Zbl 1396.68074
[103] Meseguer, J., Generalized rewrite theories, coherence completion, and symbolic methods, J. Log. Algebraic Methods Program., 110 (2020) · Zbl 1496.68166
[104] Meseguer, J.; Goguen, J. A., Order-sorted unification, J. Symb. Comput., 8, 383-413 (1989) · Zbl 0691.03002
[105] Meseguer, J.; Ölveczky, P. C., Formalization and correctness of the PALS architectural pattern for distributed real-time systems, Theor. Comp. Sci., 451, 1-37 (2012) · Zbl 1284.68073
[106] Meseguer, J.; Palomino, M.; Martí-Oliet, N., Equational abstractions, Theor. Comput. Sci., 403, 239-264 (2008) · Zbl 1155.68050
[107] Meseguer, J.; Roşu, G., The rewriting logic semantics project, Theor. Comput. Sci., 373, 213-237 (2007) · Zbl 1111.68068
[108] Meseguer, J.; Roşu, G., The rewriting logic semantics project: a progress report, Inf. Comput., 231, 38-69 (2013) · Zbl 1435.68188
[109] Meseguer, J.; Skeirik, S., Equational formulas and pattern operations in initial order-sorted algebras, Form. Asp. Comput., 29, 423-452 (2017) · Zbl 1362.68054
[110] Meseguer, J.; Talcott, C., Semantic models for distributed object reflection, (Magnusson, B., ECOOP 2002 - Object-Oriented Programming, Proceedings of the 16th European Conference. ECOOP 2002 - Object-Oriented Programming, Proceedings of the 16th European Conference, Málaga, Spain, June 10-14, 2002 (2002), Springer), 1-36 · Zbl 1049.68815
[111] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, High.-Order Symb. Comput., 20, 123-160 (2007) · Zbl 1115.68079
[112] C. Olarte, E. Pimentel, C. Rocha, Proving structural properties of sequent systems in rewriting logic, in: [121], 2018, pp. 115-135. · Zbl 1521.03059
[113] Ölveczky, P. C.; Meseguer, J., Semantics and pragmatics of Real-Time Maude, High.-Order Symb. Comput., 20, 161-196 (2007) · Zbl 1115.68095
[114] Ölveczky, P. C.; Thorvaldsen, S., Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, Theor. Comput. Sci., 410, 254-280 (2009) · Zbl 1178.68699
[115] Rocha, C.; Meseguer, J.; Muñoz, C. A., Rewriting modulo SMT and open system analysis, J. Log. Algebraic Methods Program., 86, 269-297 (2017) · Zbl 1353.68156
[116] (Roşu, G., Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications. Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008. Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications. Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008, Electronic Notes in Theoretical Computer Science, vol. 238(3) (2009), Elsevier)
[117] Roşu, G.; Ştefănescu, A., Checking reachability using matching logic, (Leavens, G. T.; Dwyer, M. B., Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012. Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012 (2012), ACM), 555-574
[118] Roşu, G.; Ştefănescu, A., From Hoare logic to matching logic reachability, (Giannakopoulou, D.; Méry, D., FM 2012: Formal Methods - Proceedings of the 18th International Symposium. FM 2012: Formal Methods - Proceedings of the 18th International Symposium, Paris, France, August 27-31, 2012 (2012), Springer), 387-402 · Zbl 1372.68066
[119] Rubio, R.; Martí-Oliet, N.; Pita, I.; Verdejo, A., Model checking strategy-controlled rewriting systems, (Geuvers, H., 4th International Conference on Formal Structures for Computation and Deduction. 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany (2019), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 18 pp · Zbl 1528.68234
[120] Rubio, R.; Martí-Oliet, N.; Pita, I.; Verdejo, A., Parameterized strategies specification in Maude, (Fiadeiro, J.; Ţuţu, I., Recent Trends in Algebraic Development Techniques, 24th IFIP WG 1.3 International Workshop. Recent Trends in Algebraic Development Techniques, 24th IFIP WG 1.3 International Workshop, WADT 2018, Egham, UK, July 2-5, 2018, Revised Selected Papers (2019), Springer), 27-44 · Zbl 1444.68104
[121] (Rusu, V., Rewriting Logic and Its Applications - Proceedings of the 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - Proceedings of the 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018. Rewriting Logic and Its Applications - Proceedings of the 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - Proceedings of the 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Lecture Notes in Computer Science, vol. 11152 (2018), Springer) · Zbl 1398.68038
[122] Sasse, R.; King, S. T.; Meseguer, J.; Tang, S., IBOS: a correct-by-construction modular browser, (Pasareanu, C. S.; Salaün, G., Formal Aspects of Component Software, 9th International Symposium. Formal Aspects of Component Software, 9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12-14, 2012, Revised Selected Papers (2013), Springer), 224-241
[123] Serbanuta, T.; Roşu, G.; Meseguer, J., A rewriting logic approach to operational semantics, Inf. Comput., 207, 305-340 (2009) · Zbl 1165.68041
[124] Skeirik, S.; Meseguer, J., Metalevel algorithms for variant satisfiability, J. Log. Algebraic Methods Program., 96, 81-110 (2018) · Zbl 1430.68423
[125] S. Skeirik, A. Ştefănescu, J. Meseguer, A constructor-based reachability logic for rewrite theories, in: [61], 2018, pp. 201-217. · Zbl 1471.68075
[126] Stehr, M., CINNI - a generic calculus of explicit substitutions and its application to lambda-, sigma- and pi-calculi, (Futatsugi, K., Proceedings of the Third International Workshop on Rewriting Logic and its Applications. Proceedings of the Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000 (2000), Elsevier), 70-92 · Zbl 0966.68147
[127] Stehr, M.; Meseguer, J., Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework, (Owe, O.; Krogdahl, S.; Lyche, T., From Object-Orientation to Formal Methods, Essays in Memory of Ole-Johan Dahl (2004), Springer), 334-375 · Zbl 1278.03066
[128] Stehr, M. O.; Meseguer, J.; Ölveczky, P. C., Rewriting logic as a unifying framework for Petri nets, (Ehrig, H.; Juhás, G.; Padberg, J.; Rozenberg, G., Unifying Petri Nets, Advances in Petri Nets (2001), Springer), 250-303 · Zbl 1017.68080
[129] Strachey, C., Fundamental concepts in programming languages, High.-Order Symb. Comput., 13, 11-49 (2000) · Zbl 0949.68510
[130] Talcott, C.; Eker, S.; Knapp, M.; Lincoln, P.; Laderoute, K., Pathway logic modeling of protein functional domains in signal transduction, (Altman, R. B.; Dunker, A. K.; Hunter, L.; Jung, T. A.; Klein, T. E., Biocomputing 2004, Proceedings of the Pacific Symposium. Biocomputing 2004, Proceedings of the Pacific Symposium, Hawaii, USA, 6-10 January 2004 (2004), World Scientific), 568-580
[131] A. Ştefănescu, S. Ciobâcă, R. Mereuta, B.M. Moore, T. Serbanuta, G. Roşu, All-path reachability logic, in: [36], 2014, pp. 425-440. · Zbl 1416.68052
[132] Ştefănescu, A.; Park, D.; Yuwen, S.; Li, Y.; Roşu, G., Semantics-based program verifiers for all languages, (Visser, E.; Smaragdakis, Y., Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30-November 4, 2016 (2016), ACM), 74-91
[133] Tushkanova, E.; Giorgetti, A.; Ringeissen, C.; Kouchnarenko, O., A rule-based system for automatic decidability and combinability, Sci. Comput. Program., 99, 3-23 (2015)
[134] Verdejo, A.; Martí-Oliet, N., Implementing CCS in Maude, (Bolognesi, T.; Latella, D., Formal Techniques for Distributed System Development, FORTE/PSTV 2000, IFIP TC6 WG6.1, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX). Formal Techniques for Distributed System Development, FORTE/PSTV 2000, IFIP TC6 WG6.1, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), October 10-13, 2000, Pisa, Italy (2000)), 351-366
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.