Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms

María Alpuente, Angel Cuenca-Ortega, Santiago Escobar, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018
EditorsPeter J. Stuckey, Fred Mesnard
PublisherSpringer-Verlag
Pages38-55
Number of pages18
ISBN (Print)9783030138370
DOIs
StatePublished - Jan 1 2019
Event28th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2018 - Frankfurt, Germany
Duration: Sep 4 2018Sep 6 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11408 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference28th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2018
CountryGermany
CityFrankfurt
Period9/4/189/6/18

Fingerprint

Associativity
Commutativity
Homeomorphic
Axioms
Modulo
Symbolic Methods
Symbolic Execution
Program Analysis
Termination
Binary
Generalise
Formulation
Experimental Results
Operator

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Alpuente, M., Cuenca-Ortega, A., Escobar, S., & Meseguer, J. (2019). Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. In P. J. Stuckey, & F. Mesnard (Eds.), Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018 (pp. 38-55). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11408 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-030-13838-7_3

Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. / Alpuente, María; Cuenca-Ortega, Angel; Escobar, Santiago; Meseguer, Jose.

Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018. ed. / Peter J. Stuckey; Fred Mesnard. Springer-Verlag, 2019. p. 38-55 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11408 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Alpuente, M, Cuenca-Ortega, A, Escobar, S & Meseguer, J 2019, Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. in PJ Stuckey & F Mesnard (eds), Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11408 LNCS, Springer-Verlag, pp. 38-55, 28th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2018, Frankfurt, Germany, 9/4/18. https://doi.org/10.1007/978-3-030-13838-7_3
Alpuente M, Cuenca-Ortega A, Escobar S, Meseguer J. Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. In Stuckey PJ, Mesnard F, editors, Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018. Springer-Verlag. 2019. p. 38-55. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-13838-7_3
Alpuente, María ; Cuenca-Ortega, Angel ; Escobar, Santiago ; Meseguer, Jose. / Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms. Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018. editor / Peter J. Stuckey ; Fred Mesnard. Springer-Verlag, 2019. pp. 38-55 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{03b10376451f49258fa92424c2324e61,
title = "Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms",
abstract = "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 increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.",
author = "Mar{\'i}a Alpuente and Angel Cuenca-Ortega and Santiago Escobar and Jose Meseguer",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-13838-7_3",
language = "English (US)",
isbn = "9783030138370",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "38--55",
editor = "Stuckey, {Peter J.} and Fred Mesnard",
booktitle = "Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018",

}

TY - GEN

T1 - Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms

AU - Alpuente, María

AU - Cuenca-Ortega, Angel

AU - Escobar, Santiago

AU - Meseguer, Jose

PY - 2019/1/1

Y1 - 2019/1/1

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 increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our 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 increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.

UR - http://www.scopus.com/inward/record.url?scp=85064047893&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85064047893&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-13838-7_3

DO - 10.1007/978-3-030-13838-7_3

M3 - Conference contribution

SN - 9783030138370

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 38

EP - 55

BT - Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018

A2 - Stuckey, Peter J.

A2 - Mesnard, Fred

PB - Springer-Verlag

ER -