×

Symbolic computation in Maude: some tapas. (English) Zbl 07496639

Fernández, Maribel (ed.), Logic-based program synthesis and transformation. 30th international symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12561, 3-36 (2021).
Summary: Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.
For the entire collection see [Zbl 1482.68019].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Order-sorted homeomorphic embedding modulo combinations of associativity and/or commutativity axioms, Fundamenta Informaticae, 177, 297-329 (2020) · Zbl 1497.68235 · doi:10.3233/FI-2020-1991
[2] Alpuente, M.; Ballis, D.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J.; Calimeri, F.; Leone, N.; Manna, M., \(ACUOS^2\): a high-performance system for modular ACU generalization with subtyping and inheritance, Logics in Artificial Intelligence, 171-181 (2019), Cham: Springer, Cham · Zbl 1525.68195 · doi:10.1007/978-3-030-19570-0_11
[3] 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, 100501 (2020) · Zbl 1494.68048 · doi:10.1016/j.jlamp.2019.100501
[4] Alpuente, M.; Escobar, S.; Espert, J.; Meseguer, J., A modular order-sorted equational generalization algorithm, Inf. Comput., 235, 98-136 (2014) · Zbl 1314.68169 · doi:10.1016/j.ic.2014.01.006
[5] Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning. Elsevier (1999) · Zbl 1011.68126
[6] Baader, F., Siekmann, J.H.: Unification theory. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 41-126. Oxford University Press (1994)
[7] Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol. 21, pp. 81-96. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013) · Zbl 1356.68140
[8] Bouchard, C.; Gero, KA; Lynch, C.; Narendran, P.; Fontaine, P.; Ringeissen, C.; Schmidt, RA, On forward closure and the finite variant property, Frontiers of Combining Systems, 327-342 (2013), Heidelberg: Springer, Heidelberg · Zbl 1398.68271 · doi:10.1007/978-3-642-40885-4_23
[9] Bouhoula, A.; Jouannaud, JP; Meseguer, J., Specification and proof in membership equational logic, Theor. Comput. Sci., 236, 35-132 (2000) · Zbl 0938.68057 · doi:10.1016/S0304-3975(99)00206-6
[10] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 1-3, 386-414 (2006) · Zbl 1097.68051 · doi:10.1016/j.tcs.2006.04.012
[11] Cholewa, A.; Escobar, S.; Meseguer, J., Constrained narrowing for conditional equational theories modulo axioms, Sci. Comput. Program., 112, 24-57 (2015) · doi:10.1016/j.scico.2015.06.001
[12] Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Department University of Illinois at Urbana-Champaign, February 2014. http://hdl.handle.net/2142/47117
[13] Ciobaca., S.: Verification of composition of security protocols with applications to electronic voting. Ph.D. thesis, ENS Cachan (2011)
[14] Clavel, M., All About Maude - A High-Performance Logical Framework (2007), Heidelberg: Springer, Heidelberg · Zbl 1115.68046 · doi:10.1007/978-3-540-71999-1
[15] Clavel, M., et al.: Maude Manual (Version 3.1), October 2020. http://maude.cs.uiuc.edu
[16] 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 · doi:10.1016/j.tcs.2006.12.009
[17] Comon, H.: Unification et disunification: Théorie et applications. Ph.D. thesis, Institute National Polytechnique de Grenoble, France (1988)
[18] Comon-Lundh, H.; Delaune, S.; Giesl, J., The finite variant property: how to get rid of some algebraic properties, Term Rewriting and Applications, 294-307 (2005), Heidelberg: Springer, Heidelberg · Zbl 1078.68059 · doi:10.1007/978-3-540-32033-3_22
[19] CVC4: https://cvc4.github.io · Zbl 1441.68235
[20] Durán, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebr. Meth. Program. 110 (2020). doi:10.1016/j.jlamp.2019.100497 · Zbl 1494.68109
[21] Durán, F.; Eker, S.; Escobar, S.; Martí-Oliet, N.; Meseguer, J.; Talcott, C.; Rusu, V., Associative unification and symbolic reasoning modulo associativity in Maude, Rewriting Logic and Its Applications, 98-114 (2018), Cham: Springer, Cham · Zbl 1475.68046 · doi:10.1007/978-3-319-99840-4_6
[22] Durán, F.; Lucas, S.; Meseguer, J.; Armando, A.; Baumgartner, P.; Dowek, G., MTT: the Maude termination tool (system description), Automated Reasoning, 313-319 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68360 · doi:10.1007/978-3-540-71070-7_27
[23] Durán, F.; Lucas, S.; Meseguer, J.; Ghilardi, S.; Sebastiani, R., Termination modulo combinations of equational theories, Frontiers of Combining Systems, 246-262 (2009), Heidelberg: Springer, Heidelberg · Zbl 1193.68145 · doi:10.1007/978-3-642-04222-5_15
[24] Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Algebraic Log. Program., 81, 816-850 (2012) · Zbl 1272.03139 · doi:10.1016/j.jlap.2011.12.004
[25] Eker, S.; Agha, G.; Danvy, O.; Meseguer, J., Fast sort computations for order-sorted matching and unification, Formal Modeling: Actors, Open Systems, Biological Systems, 299-314 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-24933-4_15
[26] Escobar, S.; Meadows, C.; Meseguer, J.; Aldini, A.; Barthe, G.; Gorrieri, R., Maude-NPA: cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design V, 1-50 (2009), Heidelberg: Springer, Heidelberg · Zbl 1252.94061 · doi:10.1007/978-3-642-03829-7_1
[27] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Algebraic Log. Program., 81, 898-928 (2012) · Zbl 1291.68217 · doi:10.1016/j.jlap.2012.01.002
[28] Fay, M.: First-order unification in an equational theory. In: Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, pp. 161-167 (1979)
[29] 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 · doi:10.1016/0304-3975(92)90302-V
[30] Gutiérrez, R.; Meseguer, J.; Fioravanti, F.; Gallagher, JP, Variant-based decidable satisfiability in initial algebras with predicates, Logic-Based Program Synthesis and Transformation, 306-322 (2018), Cham: Springer, Cham · Zbl 1508.68060 · doi:10.1007/978-3-319-94460-9_18
[31] Hendrix, J.; Meseguer, J., Order-sorted equational unification revisited, Electr. Notes Theor. Comput. Sci., 290, 37-50 (2012) · Zbl 1291.68220 · doi:10.1016/j.entcs.2012.11.010
[32] Hendrix, J.; Meseguer, J.; Ohsaki, H.; Furbach, U.; Shankar, N., A sufficient completeness checker for linear order-sorted specifications modulo axioms, Automated Reasoning, 151-155 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11814771_14
[33] Herbrand, J.: Logical Writings. Reidel (1971) · Zbl 0221.02001
[34] Hullot, J-M; Bibel, W.; Kowalski, R., Canonical forms and unification, 5th Conference on Automated Deduction Les Arcs, France, July 8-11, 1980, 318-334 (1980), Heidelberg: Springer, Heidelberg · Zbl 0441.68108 · doi:10.1007/3-540-10009-1_25
[35] Jouannaud, J-P; Kirchner, C.; Kirchner, H.; Diaz, J., Incremental construction of unification algorithms in equational theories, Automata, Languages and Programming, 361-373 (1983), Heidelberg: Springer, Heidelberg · Zbl 0516.68067 · doi:10.1007/BFb0036921
[36] Jouannaud, J.P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 257-321. MIT Press (1991)
[37] Jouannaud, JP; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 1155-1194 (1986) · Zbl 0665.03005 · doi:10.1137/0215084
[38] King, JC, Symbolic execution and program testing, Commun. ACM, 19, 7, 385-394 (1976) · Zbl 0329.68018 · doi:10.1145/360248.360252
[39] Lankford, D.S.: Canonical inference. Technical report ATP-32, Southwestn University (1975)
[40] Levi, G.; Sirovich, F.; Bečvář, J., Proving program properties, symbolic evaluation and logical procedural semantics, Mathematical Foundations of Computer Science 1975 4th Symposium, Mariánské Lázně, September 1-5, 1975, 294-301 (1975), Heidelberg: Springer, Heidelberg · Zbl 0325.68008 · doi:10.1007/3-540-07389-2_211
[41] Lucas, S.; Meseguer, J., Normal forms and normal theories in conditional rewriting, J. Log. Algebr. Meth. Program., 85, 1, 67-97 (2016) · Zbl 1356.68124 · doi:10.1016/j.jlamp.2015.06.001
[42] Makanin, GS, The problem of solvability of equations in a free semigroup, Math. USSR Sbornik, 32, 2, 129-198 (1977) · Zbl 0396.20037 · doi:10.1070/SM1977v032n02ABEH002376
[43] 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 (2002). first published as SRI Technical report SRI-CSL-93-05, August 1993 · Zbl 0912.68096
[44] Matiyasevich, YV, Hilbert’s 10th Problem (1993), Cambridge: MIT Press, Cambridge · Zbl 0790.03008
[45] McCarthy, J.; Abrahams, P.; Edwards, D.; Hart, T.; Levin, M., LISP 1.5 Programmer’s Manual (1985), Cambridge: MIT Press, Cambridge
[46] Meier, S.; Schmidt, B.; Cremers, C.; Basin, D.; Sharygina, N.; Veith, H., The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification, 696-701 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_48
[47] Meseguer, J.; Palsberg, J., Order-sorted parameterization and induction, Semantics and Algebraic Specification, 43-80 (2009), Heidelberg: Springer, Heidelberg · Zbl 1253.68215 · doi:10.1007/978-3-642-04164-8_4
[48] Meseguer, J.; Escobar, S.; Martí-Oliet, N., Variant satisfiability of parameterized strings, Rewriting Logic and Its Applications, 96-113 (2020), Cham: Springer, Cham · Zbl 1517.68165 · doi:10.1007/978-3-030-63595-4_6
[49] Meseguer, J.; Escobar, S.; Martí-Oliet, N., Variants in the infinitary unification wonderland, Rewriting Logic and Its Applications, 75-95 (2020), Cham: Springer, Cham · Zbl 1517.68164 · doi:10.1007/978-3-030-63595-4_5
[50] Meseguer, J.; Skeirik, S.; Escobar, S.; Martí-Oliet, N., Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification, Rewriting Logic and Its Applications, 114-135 (2020), Cham: Springer, Cham · Zbl 1517.68167 · doi:10.1007/978-3-030-63595-4_7
[51] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, J. Higher-Order Symbolic Comput., 20, 1-2, 123-160 (2007) · Zbl 1115.68079 · doi:10.1007/s10990-007-9000-6
[52] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[53] Meseguer, J.; Presicce, FP, Membership algebra as a logical framework for equational specification, Recent Trends in Algebraic Development Techniques, 18-61 (1998), Heidelberg: Springer, Heidelberg · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26
[54] Meseguer, J., Twenty years of rewriting logic, J. Algebraic Log. Program., 81, 721-781 (2012) · Zbl 1267.03043 · doi:10.1016/j.jlap.2012.06.003
[55] Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080 · doi:10.1016/j.tcs.2016.12.026
[56] Meseguer, J., Variant-based satisfiability in initial algebras, Sci. Comput. Program., 154, 3-41 (2018) · Zbl 1396.68074 · doi:10.1016/j.scico.2017.09.001
[57] Meseguer, J.: Generalized rewrite theories, coherence completion and symbolic methods. J. Log. Algebraic Methods Program. (2019) · Zbl 1496.68166
[58] Meseguer, J.; Goguen, J., Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems, Inf. Comput., 103, 1, 114-158 (1993) · Zbl 0796.68144 · doi:10.1006/inco.1993.1016
[59] Meseguer, J.; Goguen, J.; Smolka, G., Order-sorted unification, J. Symbolic Comput., 8, 383-413 (1989) · Zbl 0691.03002 · doi:10.1016/S0747-7171(89)80036-7
[60] Nelson, G.; Oppen, DC, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[61] Ölveczky, PC, Designing Reliable Distributed Systems (2017), London: Springer, London · Zbl 1400.68003 · doi:10.1007/978-1-4471-6687-0
[62] Oppen, DC, Complexity, convexity and combinations of theories, Theor. Comput. Sci., 12, 291-302 (1980) · Zbl 0437.03007 · doi:10.1016/0304-3975(80)90059-6
[63] Peterson, GE; Stickel, ME, Complete sets of reductions for some equational theories, J. Assoc. Comput. Mach., 28, 2, 233-264 (1981) · Zbl 0479.68092 · doi:10.1145/322248.322251
[64] Plotkin, G., Building-in equational theories, Mach. Intell., 7, 73-90 (1972) · Zbl 0262.68036
[65] Robinson, JA, A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach., 12, 23-41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253
[66] Schmidt-Schauß, M., Computational Aspects of an Order-Sorted Logic with Term Declarations (1989), Heidelberg: Springer, Heidelberg · Zbl 0689.68001 · doi:10.1007/BFb0024065
[67] Seidenberg, A., A new decision method for elementary algebra, Ann. Math., 60, 365-374 (1954) · Zbl 0056.01804 · doi:10.2307/1969640
[68] Skeirik, S.; Meseguer, J., Metalevel algorithms for variant satisfiability, J. Log. Algebr. Meth. Program., 96, 81-110 (2018) · Zbl 1430.68423 · doi:10.1016/j.jlamp.2017.12.006
[69] Skeirik, S.; Stefanescu, A.; Meseguer, J., A constructor-based reachability logic for rewrite theories, Fundam. Inform., 173, 4, 315-382 (2020) · Zbl 1471.68076 · doi:10.3233/FI-2020-1926
[70] Slagle, JR, Automated theorem-proving for theories with simplifiers commutativity, and associativity, J. ACM, 21, 4, 622-642 (1974) · Zbl 0296.68092 · doi:10.1145/321850.321859
[71] Smolka, G., Nutt, W., Goguen, J., Meseguer, J.: Order-sorted equational computation. In: Nivat, M., Aït-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 297-367. Academic Press (1989)
[72] Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951). prepared with the assistance of J.C.C. McKinsey · Zbl 0044.25102
[73] Viry, P., Equational rules for rewriting logic, Theor. Comput. Sci., 285, 487-517 (2002) · Zbl 1001.68058 · doi:10.1016/S0304-3975(01)00366-8
[74] Yices: https://yices.csl.sri.com
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.