Optimizing Maude programs via program specialization

DOI10.1007/978-3-031-31476-6_2zbMath1529.68130MaRDI QIDQ6175104

José Meseguer, Demis Ballis, Santiago Escobar, María Alpuente, Julia Sapiña

Publication date: 17 August 2023

Published in: Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems (Search for Journal in Brave)

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• Termination of narrowing revisited
• Conditional rewriting logic as a unified model of concurrency
• Equational rules for rewriting logic
• Folding variant narrowing and optimal variant termination
• 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
• A modular order-sorted equational generalization algorithm
• 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
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Specialization of functional logic programs based on needed narrowing
• MTT: The Maude Termination Tool (System Description)
• Partial evaluation in logic programming
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• A Transformation System for Developing Recursive Programs
• Assertion-based analysis via slicing withABETS(system description)
• Variant-Based Satisfiability in Initial Algebras
• Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
• Variant Narrowing and Equational Unification
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Term Rewriting and Applications

This page was built for publication: Optimizing Maude programs via program specialization