- -

Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Alpuente;Cuenca-O ...
Tamaño: 443.2Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: fi-177(3-4)05ACEM ...
Tamaño: 323.5Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Alpuente Frasnedo, María es_ES
dc.contributor.author Cuenca-Ortega, Angel es_ES
dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Meseguer, José es_ES
dc.date.accessioned 2021-02-13T04:31:52Z
dc.date.available 2021-02-13T04:31:52Z
dc.date.issued 2020 es_ES
dc.identifier.issn 0169-2968 es_ES
dc.identifier.uri http://hdl.handle.net/10251/161203
dc.description.abstract [EN] 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-sorted 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. es_ES
dc.description.sponsorship M. Alpuente and S. Escobar have been partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grant PROMETEO/2019/098, and by the European Union's Horizon 2020 research and innovation programme under grant agreement No. 952215 (TAILOR). J. Meseguer has been supported by NRL under contract number N00173-17-1-G002. A. Cuenca-Ortega has been supported by the SENESCYT, Ecuador (scholarship program 2013). es_ES
dc.language Inglés es_ES
dc.publisher IOS Press es_ES
dc.relation.ispartof Fundamenta Informaticae es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Homeomorphic embedding es_ES
dc.subject Rewriting logic es_ES
dc.subject Maude es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.3233/FI-2020-1991 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NRL//N00173-17-1-G002/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/EC/H2020/952215/EU/Foundations of Trustworthy AI - Integrating Reasoning, Learning and Optimization/
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Alpuente Frasnedo, M.; Cuenca-Ortega, A.; Escobar Román, S.; Meseguer, J. (2020). Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms. Fundamenta Informaticae. 177(3-4):297-329. https://doi.org/10.3233/FI-2020-1991 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.3233/FI-2020-1991 es_ES
dc.description.upvformatpinicio 297 es_ES
dc.description.upvformatpfin 329 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 177 es_ES
dc.description.issue 3-4 es_ES
dc.relation.pasarela S\403095 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder U.S. Naval Research Laboratory es_ES
dc.contributor.funder Agencia Estatal de Investigación es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Secretaría de Educación Superior, Ciencia, Tecnología e Innovación, Ecuador es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem