Symbolic Specialization of Rewriting Logic Theories with Presto
From MaRDI portal
Publication:6063888
DOI10.1017/s1471068421000600zbMath1530.68130arXiv2112.10201OpenAlexW4211212743MaRDI QIDQ6063888
Julia Sapiña, Santiago Escobar, María Alpuente, Demis Ballis
Publication date: 12 December 2023
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2112.10201
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Normal forms and normal theories in conditional rewriting
- Debugging Maude programs via runtime assertion checking and trace slicing
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Equational abstractions
- A compact fixpoint semantics for term rewriting systems
- Type-based homeomorphic embedding for online termination
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Termination of narrowing revisited
- Conditional rewriting logic as a unified model of concurrency
- Equational rules for rewriting logic
- Rewriting logic: Roadmap and bibliography
- Folding variant narrowing and optimal variant termination
- Symbolic computation in Maude: some tapas
- Order-sorted equational generalization algorithm revisited
- Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system
- 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
- 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
- A modular order-sorted equational generalization algorithm
- Optimization of rewrite theories by equational partial evaluation
- On Forward Closure and the Finite Variant Property
- Backward Trace Slicing for Conditional Rewrite Theories
- Conditional Narrowing Modulo in Rewriting Logic and Maude
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- The NRL Protocol Analyzer: An Overview
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Specialization of functional logic programs based on needed narrowing
- Computationally Equivalent Elimination of Conditions
- MTT: The Maude Termination Tool (System Description)
- A Modular Equational Generalization Algorithm
- Partial evaluation in logic programming
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- A Transformation System for Developing Recursive Programs
- The integration of functions into logic programming: From theory to practice
- Variant-Based Satisfiability in Initial Algebras
- Conjunctive partial deduction: foundations, control, algorithms, and experiments
- Order-Sorted Generalization
- Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
- Symbolic Analysis of Maude Theories with Narval
- The applicability of logic program analysis and transformation to theorem proving
- Functional Logic Programming in Maude
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
This page was built for publication: Symbolic Specialization of Rewriting Logic Theories with Presto
