Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
From MaRDI portal
Publication:2104541
DOI10.1007/978-3-031-10769-6_31OpenAlexW4289104034WikidataQ123905802 ScholiaQ123905802MaRDI QIDQ2104541FDOQ2104541
Rubén Rubio, Steven Eker, Carolyn 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
Cites Work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
- Z3str2: an efficient solver for strings, regular expressions, and length constraints
- 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
- A Machine-Oriented Logic Based on the Resolution Principle
- Complete Sets of Reductions for Some Equational Theories
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Title not available (Why is that?)
- Paramodulation-based theorem proving
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Title not available (Why is that?)
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Semantics and pragmatics of real-time maude
- Title not available (Why is that?)
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Term Rewriting and Applications
- Title not available (Why is that?)
- Folding variant narrowing and optimal variant termination
- Matching, unification and complexity
- Strict coherence of conditional rewriting modulo axioms
- Variant-Based Satisfiability in Initial Algebras
- Reflective metalogical frameworks
- Title not available (Why is that?)
- Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
- Proving Safety Properties of Rewrite Theories
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Symbolic reasoning methods in rewriting logic and Maude
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Programming and symbolic computation in Maude
- Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
- A Constructor-Based Reachability Logic for Rewrite Theories
- Symbolic computation in Maude: some tapas
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Ground confluence of order-sorted conditional specifications modulo axioms
- Metalevel algorithms for variant satisfiability
- Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
Cited In (5)
- Building correct-by-construction systems with formal patterns
- Maude
- Verification of the ROS NavFn planner using executable specification languages
- Variants and satisfiability in the infinitary unification wonderland
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
Uses Software
This page was built for publication: Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104541)
