{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T18:40:47Z","timestamp":1791484847521,"version":"4.3.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["FI"],"published-print":{"date-parts":[[2020,12,10]]},"abstract":"<jats:p>The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order\u2013sorted rewrite theories that may contain various combinations of associativity and\/or commutativity axioms for different binary operators. We systematically measure the performance of different, increasingly efficient formulations of the homeomorphic embedding relation modulo axioms that we implement in Maude. Our experimental results show that the most efficient version indeed pays off in practice.<\/jats:p>","DOI":"10.3233\/fi-2020-1991","type":"journal-article","created":{"date-parts":[[2020,12,11]],"date-time":"2020-12-11T12:34:51Z","timestamp":1607690091000},"page":"297-329","source":"Crossref","is-referenced-by-count":5,"title":["Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and\/or Commutativity Axioms*"],"prefix":"10.1177","volume":"177","author":[{"given":"Mar\u00eda","family":"Alpuente","sequence":"first","affiliation":[{"name":"VRAIN, Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e9ncia, Spain. alpuente@upv.es"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Angel","family":"Cuenca-Ortega","sequence":"additional","affiliation":[{"name":"Universidad de Guayaquil, Guayaquil, Ecuador. angel.cuencao@ug.edu.ec"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[{"name":"VRAIN, Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e9ncia, Spain. sescobar@upv.es"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA. meseguer@illinois.edu"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"179","container-title":["Fundamenta Informaticae"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/FI-2020-1991","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:32:13Z","timestamp":1777444333000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/FI-2020-1991"}},"subtitle":[],"editor":[{"given":"Manuel","family":"Hermenegildo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"editor"}]},{"given":"Pedro","family":"L\u00f3pez-Garc\u00eda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"editor"}]},{"given":"Alberto","family":"Pettorossi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"editor"}]},{"given":"Maurizio","family":"Proietti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"editor"}]}],"short-title":[],"issued":{"date-parts":[[2020,12,10]]},"references-count":0,"journal-issue":{"issue":"3-4"},"URL":"https:\/\/doi.org\/10.3233\/fi-2020-1991","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12,10]]}}}