Programming and symbolic computation in Maude
From MaRDI portal
Abstract: Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper.
Recommendations
- Symbolic computation in Maude: some tapas
- Symbolic computation in automated program reasoning
- Symbolic computing
- Maude: specification and programming in rewriting logic
- Functional logic programming in Maude
- Symbolic computation via program transformation
- scientific article; zbMATH DE number 1639657
- Polytypic programming in Maude
Cites work
- scientific article; zbMATH DE number 1696588 (Why is no real title available?)
- scientific article; zbMATH DE number 1696904 (Why is no real title available?)
- scientific article; zbMATH DE number 4130339 (Why is no real title available?)
- scientific article; zbMATH DE number 2089377 (Why is no real title available?)
- scientific article; zbMATH DE number 3817070 (Why is no real title available?)
- scientific article; zbMATH DE number 3945331 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 3703962 (Why is no real title available?)
- scientific article; zbMATH DE number 1231537 (Why is no real title available?)
- scientific article; zbMATH DE number 1231664 (Why is no real title available?)
- scientific article; zbMATH DE number 1231673 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1973125 (Why is no real title available?)
- scientific article; zbMATH DE number 7559300 (Why is no real title available?)
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- A constructor-based reachability logic for rewrite theories
- A generic framework for symbolic execution: a coinductive approach
- A modular order-sorted equational generalization algorithm
- A partial evaluation framework for order-sorted equational programs modulo axioms
- A rewriting logic approach to operational semantics
- A rewriting semantics for Maude strategies
- Abstract logical model checking of infinite-state systems using narrowing
- Algebraic and logic programming. Third international conference, ALP '92, Volterra, Italy, September 2--4, 1992. Proceedings
- Algorithm = logic + control
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Associative unification and symbolic reasoning modulo associativity in Maude
- Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
- Built-in variant generation and unification, and their applications in Maude 2.7
- CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi
- Conditional rewriting logic as a unified model of concurrency
- Deduction, strategies, and rewriting
- Equality, types, modules, and (why not?) generics for logic programming
- Equational abstractions
- Equational formulas and pattern operations in initial order-sorted algebras
- Folding variant narrowing and optimal variant termination
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- Formalization and correctness of the PALS architectural pattern for distributed real-time systems
- From hoare logic to matching logic reachability
- Functional logic programming in Maude
- Fundamental concepts in programming languages
- Generalized rewrite theories and coherence completion
- Generalized rewrite theories, coherence completion, and symbolic methods
- Ground confluence of order-sorted conditional specifications modulo axioms
- IThe 2nd international workshop on rewriting logic and its applications, RWLW.. Abbaye des Prèmontrès at Pont-á-Mousson, France, September 1998
- Infinite-state model checking of LTLR formulas using narrowing
- Institutions: abstract model theory for specification and programming
- Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday
- Logic-based program synthesis and transformation. 27th international symposium, LOPSTR 2017, Namur, Belgium, October 10--12, 2017. Revised selected papers
- Maude's module algebra
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Maude: specification and programming in rewriting logic
- Metalevel algorithms for variant satisfiability
- Modular structural operational semantics with strategies
- Normal forms and normal theories in conditional rewriting
- On sentences which are true of direct unions of algebras
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Order-Sorted Parameterization and Induction
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Order-sorted equational unification revisited
- Order-sorted unification
- Parameterized strategies specification in Maude
- Partial evaluation of order-sorted equational programs modulo axioms
- Predicate abstraction of rewrite theories
- Proving operational termination of membership equational programs
- Proving structural properties of sequent systems in rewriting logic
- Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
- Reflection in conditional rewriting logic
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Rewriting and typed lambda calculi. Joint international conference, RTA-TLCA 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings
- Rewriting logic and its applications. 12th international workshop, WRLA 2018, held as a satellite event of ETAPS, Thessaloniki, Greece, June 14--15, 2018. Proceedings
- Rewriting logic as a semantic framework for concurrency: a progress report
- Rewriting modulo SMT and open system analysis
- Rewriting semantics of production rule sets
- Semantic foundations for generalized rewrite theories
- Semantics and pragmatics of real-time maude
- Specification and proof in membership equational logic
- State space reduction in the Maude-NRL protocol analyzer
- Strategies and simulations in a semantic framework
- Strict coherence of conditional rewriting modulo axioms
- Structured theories and institutions
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Symbolic reasoning methods in rewriting logic and Maude
- Term Rewriting and Applications
- The Temporal Logic of Rewriting: A Gentle Introduction
- The rewriting logic semantics project
- The rewriting logic semantics project: a progress report
- Twenty years of rewriting logic
- Two Decades of Maude
- Using Maude and its strategies for defining a framework for analyzing Eden semantics
- Variant-Based Satisfiability in Initial Algebras
- Variant-based decidable satisfiability in initial algebras with predicates
- Variants, unification, narrowing, and symbolic reachability in Maude 2.6
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
Cited in
(38)- Symbolic computation in Maude: some tapas
- Building correct-by-construction systems with formal patterns
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Towards Maude 2. 0
- Local confluence of conditional and generalized term rewriting systems
- scientific article; zbMATH DE number 1973990 (Why is no real title available?)
- Hardware Trojan detection via rewriting logic
- Strategies and simulations in a semantic framework
- Applications and extensions of context-sensitive rewriting
- Optimizing Maude programs via program specialization
- Strategies in conditional narrowing modulo SMT plus axioms
- scientific article; zbMATH DE number 2043522 (Why is no real title available?)
- An Overview of the Maude Strategy Language and its Applications
- Symbolic Specialization of Rewriting Logic Theories with Presto
- Integrating Maude into Hets
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- Symbolic analysis of Maude theories with Narval
- Prototyping 3APL in the Maude Term Rewriting Language
- Variants, unification, narrowing, and symbolic reachability in Maude 2.6
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Metalevel transformation of strategies
- Guest editor's foreword
- Functional logic programming in Maude
- Symbolic reasoning methods in rewriting logic and Maude
- Mathemagix: Towards Large Scale Programming for Symbolic and Certified Numeric Computations
- Maude2Lean: theorem proving for Maude specifications using Lean
- QMaude: quantitative specification and verification in rewriting logic
- Maude: specification and programming in rewriting logic
- Safety enforcement via programmable strategies in Maude
- Verification of the ROS NavFn planner using executable specification languages
- Formalization and analysis of the post-quantum signature scheme FALCON with Maude
- Variants and satisfiability in the infinitary unification wonderland
- Derivational complexity and context-sensitive Rewriting
- The Maude strategy language
- Built-in variant generation and unification, and their applications in Maude 2.7
- A Maude environment for CafeOBJ
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
Describes a project that uses
Uses Software
This page was built for publication: Programming and symbolic computation in Maude
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2291818)
