Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
type: Item
instance of: scholarly article
title: Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
DOI: 10.1007/978-3-031-10769-6_31
author: Francisco Durán
author: Steven Eker
author: Santiago Escobar
author: Narciso Martí-Oliet
author: José Meseguer
author: Rubén Rubio
author: Carolyn Talcott
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628207
describes a project that uses: Maude-NPA
describes a project that uses: TAMARIN
describes a project that uses: Z3str2
describes a project that uses: ACUOS2
describes a project that uses: Akiss
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 31
OpenAlex ID: W4289104034
Wikidata QID: Q123905802
cites work: Q4797044
cites work: \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
cites work: Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
cites work: A partial evaluation framework for order-sorted equational programs modulo axioms
cites work: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
cites work: Reflective metalogical frameworks
cites work: Automated Verification of Equivalence Properties of Cryptographic Protocols
cites work: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
cites work: Term Rewriting and Applications
cites work: Q4385532
cites work: Programming and symbolic computation in Maude
cites work: Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
cites work: Ground confluence of order-sorted conditional specifications modulo axioms
cites work: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
cites work: Symbolic Model Checking of Infinite-State Systems Using Narrowing
cites work: Folding variant narrowing and optimal variant termination
cites work: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
cites work: Matching, unification and complexity
cites work: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
cites work: The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
cites work: Q4222859
cites work: Q3839051
cites work: Strict coherence of conditional rewriting modulo axioms
cites work: Symbolic reasoning methods in rewriting logic and Maude
cites work: Variant-Based Satisfiability in Initial Algebras
cites work: Symbolic computation in Maude: some tapas
cites work: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
cites work: Paramodulation-based theorem proving
cites work: Semantics and pragmatics of real-time maude
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Proving Safety Properties of Rewrite Theories
cites work: Metalevel algorithms for variant satisfiability
cites work: A Constructor-Based Reachability Logic for Rewrite Theories
cites work: Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
cites work: A mechanical solution of Schubert's steamroller by many-sorted resolution
cites work: Z3str2: an efficient solver for strings, regular expressions, and length constraints
description: scientific article; zbMATH DE number 7628207