Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms

María Alpuente, Angel Cuenca-Ortega, Santiago Escobar, José 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 Berlin Heidelberg
Pages38-55
Number of pages18
ISBN (Print)9783030138370
DOIs
StatePublished - 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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms'. Together they form a unique fingerprint.

Cite this