Abstract
This paper introduces some novel features of Maude 2.7. We have added support for: (i) built-in order-sorted unification modulo associativity, commutativity, and identity, (ii) built-in variant generation, (iii) built-in order-sorted unification modulo a finite variant theory, and (iv) symbolic reachability modulo a finite variant theory.
F. Durán was partially supported by Spanish MINECO under grant TIN 2014-52034-R and Universidad de Málaga (Campus de Excelencia Internacional Andalucía Tech). S. Eker and C. Talcott were partially supported by NSF grant CNS-1318848. S. Escobar was partially supported by Spanish MINECO under grants TIN 2015-69175-C4-1-R and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana under grant PROMETEOII/2015/013. N. Martí-Oliet was partially supported by Spanish MINECO under grant StrongSoft (TIN 2012-39391-C04-04) and Comunidad de Madrid program N-GREENS Software (S2013/ICE-2731). J. Meseguer was partially supported by NSF grant CNS-1319109.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Maude is publicly available at http://maude.cs.illinois.edu.
References
Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F., (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24–26, 2013, Eindhoven, The Netherlands. LIPIcs vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)
Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On forward closure and the finite variant property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 327–342. Springer, Heidelberg (2013)
Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, University of Illinois at Urbana-Champaign (2014). http://hdl.handle.net/2142/47117
Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Unification and narrowing in maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 380–390. Springer, Heidelberg (2009)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)
Durán, F., Eker, S., Escobar, S., Meseguer, J., Talcott, C.L.: Variants, unification, narrowing, and symbolic reachability inMaude 2.6. In: Schmidt-Schauß, M., (ed.) Proceedings of the 22ndInternational Conference on Rewriting Techniques and Applications, RTA2011, May 30 - June 1, 2011, Novi Sad, Serbia. LIPIcs, vol. 10, pp. 31–40. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)
Durán, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 246–262. Springer, Heidelberg (2009)
Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Logic Algebraic Program. 81(7–8), 816–850 (2012)
Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equationalproperties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)
Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Logic Algebraic Program. 81(7–8), 898–928 (2012)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)
Meseguer, J.: Variant-based satisfiability in initial algebras. Technical report, University of Illinois at Urbana-Champaign (2015). http://hdl.handle.net/2142/88408
Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High. Order Symbolic Comput. 20(1–2), 123–160 (2007)
Riesco, A.: Using big-step and small-step semantics in maude to perform declarative debugging. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 52–68. Springer, Heidelberg (2014)
Rusu, V.: Combining theorem proving and narrowing for rewriting-logic specifications. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 135–150. Springer, Heidelberg (2010)
Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. Sci. Comput. Program. 99, 3–23 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Talcott, C. (2016). Built-in Variant Generation and Unification, and Their Applications in Maude 2.7. In: Olivetti, N., Tiwari, A. (eds) Automated Reasoning. IJCAR 2016. Lecture Notes in Computer Science(), vol 9706. Springer, Cham. https://doi.org/10.1007/978-3-319-40229-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-40229-1_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40228-4
Online ISBN: 978-3-319-40229-1
eBook Packages: Computer ScienceComputer Science (R0)