Symbolic computation in Maude: some tapas
From MaRDI portal
Publication:2119100
DOI10.1007/978-3-030-68446-4_1OpenAlexW3130775410MaRDI QIDQ2119100
Publication date: 23 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_1
Related Items (2)
Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Order-sorted unification
- Strict coherence of conditional rewriting modulo axioms
- Normal forms and normal theories in conditional rewriting
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Complexity, convexity and combinations of theories
- Conditional rewriting logic as a unified model of concurrency
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Equational rules for rewriting logic
- Variant-based decidable satisfiability in initial algebras with predicates
- Computational aspects of an order-sorted logic with term declarations
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Specification and proof in membership equational logic
- DRAT-based bit-vector proofs in CVC4
- Generalized rewrite theories, coherence completion, and symbolic methods
- Programming and symbolic computation in Maude
- A partial evaluation framework for order-sorted equational programs modulo axioms
- \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
- Metalevel algorithms for variant satisfiability
- A modular order-sorted equational generalization algorithm
- Semantic foundations for generalized rewrite theories
- A new decision method for elementary algebra
- Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
- On Forward Closure and the Finite Variant Property
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Order-Sorted Parameterization and Induction
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- MTT: The Maude Termination Tool (System Description)
- Termination Modulo Combinations of Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Simplification by Cooperating Decision Procedures
- Complete Sets of Reductions for Some Equational Theories
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Symbolic execution and program testing
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
- 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
- Order-sorted Equational Unification Revisited
- A Machine-Oriented Logic Based on the Resolution Principle
- Term Rewriting and Applications
- Designing reliable distributed systems. A formal methods approach based on executable modeling in Maude
This page was built for publication: Symbolic computation in Maude: some tapas
