{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:49:55Z","timestamp":1778914195209,"version":"3.51.4"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T00:00:00Z","timestamp":1503532800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces<jats:monospace>GLINTS<\/jats:monospace>, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity. This novel equational unification relies on built-in generation of the set of<jats:italic>variants<\/jats:italic>of a term<jats:italic>t<\/jats:italic>, i.e., the canonical form of<jats:italic>t<\/jats:italic>\u03c3 for a computed substitution \u03c3. Variant generation relies on a novel narrowing strategy called<jats:italic>folding variant narrowing<\/jats:italic>that opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies the<jats:italic>finite variant property<\/jats:italic>, i.e., there is a finite number of most general variants for every term in the theory. However, variant narrowing computations can be extremely involved and are simply presented in text format by Maude, often being too heavy to be debugged or even understood. The<jats:monospace>GLINTS<\/jats:monospace>system provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of node<jats:italic>embedding<\/jats:italic>and<jats:italic>closedness<\/jats:italic>modulo axioms, and (iv) querying and inspecting selected parts of the variant trees.<\/jats:p>","DOI":"10.1017\/s147106841700031x","type":"journal-article","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T04:44:19Z","timestamp":1503549859000},"page":"689-707","source":"Crossref","is-referenced-by-count":4,"title":["Inspecting Maude variants with<tt>GLINTS<\/tt>"],"prefix":"10.1017","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9268-1178","authenticated-orcid":false,"given":"M.","family":"ALPUENTE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"ESCOBAR","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2994-6986","authenticated-orcid":false,"given":"J.","family":"SAPI\u00d1A","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7798-611X","authenticated-orcid":false,"given":"A.","family":"CUENCA-ORTEGA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2017,8,24]]},"reference":[{"key":"S147106841700031X_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291896"},{"key":"S147106841700031X_ref15","unstructured":"Erbatur S. , Escobar S. , Kapur D. , Liu Z. , Lynch C. , Meadows C. , Meseguer J. , Narendran P. , Santiago S. and Sasse R. 2012. Effective symbolic protocol analysis via equational irreducibility conditions. In Proc. of the 17th European Symposium on Research in Computer Security (ESORICS 2012). Lecture Notes in Computer Science, vol. 7459. Springer, 73\u201390."},{"key":"S147106841700031X_ref21","unstructured":"Meier S. , Schmidt B. , Cremers C. and Basin D. A. 2013. The TAMARIN prover for the symbolic analysis of security protocols. In Proc. of the 25th International Conference on Computer Aided Verification (CAV 2013). Lecture Notes in Computer Science, vol. 8044. Springer, 696\u2013701."},{"key":"S147106841700031X_ref7","unstructured":"Bouchard C. , Gero K. A. , Lynch C. and Narendran P. 2013. On forward closure and the finite variant property. In Proc. of the 9th International Symposium on Frontiers of Combining Systems (FroCos 2013). Lecture Notes in Computer Science, vol. 8152. Springer, 327\u2013342."},{"key":"S147106841700031X_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37651-1_6"},{"key":"S147106841700031X_ref19","first-page":"379","volume-title":"The Essence of Computation. Essays Dedicated to Neil D. Jones on the Occasion of his 60th Birthday","author":"Leuschel","year":"2002"},{"key":"S147106841700031X_ref2","unstructured":"Alpuente M. , Cuenca-Ortega A. , Escobar S. and Meseguer J. 2017. Partial evaluation of order-sorted equational programs modulo axioms. In Proc. of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Lecture Notes in Computer Science, vol. 10184. Springer, 3\u201320."},{"key":"S147106841700031X_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/289121.289130"},{"key":"S147106841700031X_ref26","unstructured":"Yang F. , Escobar S. , Meadows C. , Meseguer J. and Narendran P. 2011. Theories of homomorphic encryption, unification, and the finite variant property. In Proc. of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014). ACM Press, 123\u2013133."},{"key":"S147106841700031X_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"S147106841700031X_ref3","unstructured":"Alpuente M. , Falaschi M. , Moreno G. and Vidal G. 1997. Safe folding\/unfolding with conditional narrowing. In Proc. of the 6th International Joint Conference on Algebraic and Logic Programming (ALP 1997). Lecture Notes in Computer Science, vol. 1298. Springer, 1\u201315."},{"key":"S147106841700031X_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"S147106841700031X_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.12.004"},{"key":"S147106841700031X_ref9","unstructured":"Clavel M. , Dur\u00e1n F. , Eker S. , Escobar S. , Lincoln P. , Mart\u00ed-Oliet N. , Meseguer J. and Talcott C. 2016 Maude Manual (Version 2.7.1). Technical Report, SRI International Computer Science Lab."},{"key":"S147106841700031X_ref24","unstructured":"Meseguer T. 2006. From OBJ to Maude and beyond. In Proc. of Algebra, Meaning, and Computation. Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday. Lecture Notes in Computer Science, vol. 4060. Springer, 252\u2013280."},{"key":"S147106841700031X_ref25","doi-asserted-by":"crossref","unstructured":"Pettorossi A. and Proietti M. 1996. A comparative revisitation of some program transformation techniques. In Proc. of International Dagstuhl Seminar on Partial Evaluation. Lecture Notes in Computer Science, vol. 1110. Springer, 355\u2013385.","DOI":"10.1007\/3-540-61580-6_18"},{"key":"S147106841700031X_ref12","unstructured":"Dur\u00e1n F. , Eker S. , Escobar S. , Mart\u00ed-Oliet N. , Meseguer J. and Talcott C. 2016. Built-in variant generation and unification, and their applications in maude 2.7. In Proc. of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016). Lecture Notes in Computer Science, vol. 9706. Springer, 183\u2013192."},{"key":"S147106841700031X_ref20","unstructured":"Mau-Dev 2016. The Mau-Dev Web site. URL: http:\/\/safe-tools.dsic.upv.es\/maudev. [Accessed on July 2017]."},{"key":"S147106841700031X_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227597"},{"key":"S147106841700031X_ref13","unstructured":"Dur\u00e1n F. , Lucas S. and Meseguer J. 2009. Termination modulo combinations of equational theories. In Proc. of the 7th International Symposium on Frontiers of Combining Systems (FroCos 2009). Lecture Notes in Computer Science, vol. 5749. Springer, 246\u2013262."},{"key":"S147106841700031X_ref16","unstructured":"Escobar S. , Meadows C. and Meseguer J. 2009. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V (FOSAD 2007\/2008\/2009 Tutorial Lectures). Lecture Notes in Computer Science, vol. 5705. Springer, 1\u201350."},{"key":"S147106841700031X_ref10","doi-asserted-by":"crossref","unstructured":"Comon-Lundh H. and Delaune S. 2005. The finite variant property: How to get Rid of some algebraic properties. In Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005). Lecture Notes in Computer Science, vol. 3467. Springer, 294\u2013307.","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"S147106841700031X_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068416000375"},{"key":"S147106841700031X_ref23","unstructured":"Meseguer J. 2015. Variant-based satisfiability in initial algebras. In Proc. of the 4th International Workshop for Safety-Critical Systems (FTSCS 2015). Communications in Computer and Information Science, vol. 596. Springer, 3\u201334."},{"key":"S147106841700031X_ref6","unstructured":"Bae K. , Escobar S. and Meseguer J. 2013. Abstract logical model checking of infinite-state systems using narrowing. In Proc. of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), LIPIcs, vol. 21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 81\u201396."},{"key":"S147106841700031X_ref11","volume-title":"Analysis and Visualization Tools for Constraint Programming: Constraint Debugging","author":"Deransart","year":"2006"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S147106841700031X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T15:01:29Z","timestamp":1570028489000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S147106841700031X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,24]]},"references-count":26,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["S147106841700031X"],"URL":"https:\/\/doi.org\/10.1017\/s147106841700031x","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,24]]}}}