TY - JOUR
T1 - Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms
AU - Alpuente, María
AU - Cuenca-Ortega, Angel
AU - Escobar, Santiago
AU - Meseguer, José
N1 - Publisher Copyright:
© 2020-IOS Press and the authors. All rights reserved.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
KW - homeomorphic embedding
KW - Maude
KW - rewriting logic
UR - http://www.scopus.com/inward/record.url?scp=85097872754&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85097872754&partnerID=8YFLogxK
U2 - 10.3233/FI-2020-1991
DO - 10.3233/FI-2020-1991
M3 - Article
AN - SCOPUS:85097872754
VL - 177
SP - 297
EP - 329
JO - Fundamenta Informaticae
JF - Fundamenta Informaticae
SN - 0169-2968
IS - 3-4
ER -