Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

DOI10.1007/978-3-031-10769-6_31OpenAlexW4289104034WikidataQ123905802 ScholiaQ123905802MaRDI QIDQ2104541

Rubén Rubio, Steven Eker, Carolyn L. Talcott, Santiago Escobar, Narciso Martí-Oliet, Francisco Durán, José Meseguer

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_31

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Variants and satisfiability in the infinitary unification wonderland ⋮ Verification of the ROS NavFn planner using executable specification languages ⋮ Maude ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems

Uses Software

• Maude-NPA
• Akiss
• TAMARIN
• Z3str2
• ACUOS2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Strict coherence of conditional rewriting modulo axioms
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Semantics and pragmatics of real-time maude
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
• Symbolic reasoning methods in rewriting logic and Maude
• Folding variant narrowing and optimal variant termination
• Symbolic computation in Maude: some tapas
• The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
• Programming and symbolic computation in Maude
• A partial evaluation framework for order-sorted equational programs modulo axioms
• Ground confluence of order-sorted conditional specifications modulo axioms
• \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
• Metalevel algorithms for variant satisfiability
• Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Matching, unification and complexity
• Proving Safety Properties of Rewrite Theories
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Complete Sets of Reductions for Some Equational Theories
• Variant-Based Satisfiability in Initial Algebras
• Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
• A Constructor-Based Reachability Logic for Rewrite Theories
• Reflective metalogical frameworks
• Automated Verification of Equivalence Properties of Cryptographic Protocols
• Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• A Machine-Oriented Logic Based on the Resolution Principle
• Term Rewriting and Applications

This page was built for publication: Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)