Programming and symbolic computation in Maude
From MaRDI portal
Publication:2291818
DOI10.1016/j.jlamp.2019.100497zbMath1494.68109arXiv1910.08416OpenAlexW3105106018WikidataQ123905806 ScholiaQ123905806MaRDI QIDQ2291818
Steven Eker, Francisco Durán, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn L. Talcott, Santiago Escobar
Publication date: 31 January 2020
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1910.08416
unificationsymbolic model checkingnarrowingstrategiesrewriting logicMaudeexternal objectsmeta-interpreters
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)
Related Items
Hardware Trojan detection via rewriting logic, Metalevel transformation of strategies, An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis, Symbolic Specialization of Rewriting Logic Theories with Presto, Variants and satisfiability in the infinitary unification wonderland, The Maude strategy language, Local confluence of conditional and generalized term rewriting systems, QMaude: quantitative specification and verification in rewriting logic, Strategies in conditional narrowing modulo SMT plus axioms, Optimizing Maude programs via program specialization, Safety enforcement via programmable strategies in Maude, Verification of the ROS NavFn planner using executable specification languages, Unnamed Item, Guest editor's foreword, A partial evaluation framework for order-sorted equational programs modulo axioms, Applications and extensions of context-sensitive rewriting, Derivational complexity and context-sensitive Rewriting, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Symbolic computation in Maude: some tapas
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rewriting modulo SMT and open system analysis
- The rewriting logic semantics project: a progress report
- State space reduction in the Maude-NRL protocol analyzer
- Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday
- A generic framework for symbolic execution: a coinductive approach
- Order-sorted unification
- Strict coherence of conditional rewriting modulo axioms
- Formalization and correctness of the PALS architectural pattern for distributed real-time systems
- Normal forms and normal theories in conditional rewriting
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- The rewriting logic semantics project
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Semantics and pragmatics of real-time maude
- Maude's module algebra
- Equational abstractions
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- A rewriting logic approach to operational semantics
- Conditional rewriting logic as a unified model of concurrency
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- IThe 2nd international workshop on rewriting logic and its applications, RWLW.. Abbaye des Prèmontrès at Pont-á-Mousson, France, September 1998
- Fundamental concepts in programming languages
- Maude: specification and programming in rewriting logic
- Reflection in conditional rewriting logic
- Logic-based program synthesis and transformation. 27th international symposium, LOPSTR 2017, Namur, Belgium, October 10--12, 2017. Revised selected papers
- A constructor-based reachability logic for rewrite theories
- Variant-based decidable satisfiability in initial algebras with predicates
- Rewriting logic and its applications. 12th international workshop, WRLA 2018, held as a satellite event of ETAPS, Thessaloniki, Greece, June 14--15, 2018. Proceedings
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Symbolic reasoning methods in rewriting logic and Maude
- Structured theories and institutions
- 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
- Rewriting semantics of production rule sets
- Specification and proof in membership equational logic
- Parameterized strategies specification in Maude
- 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
- Proving operational termination of membership equational programs
- Generalized rewrite theories, coherence completion, and symbolic methods
- 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
- Partial evaluation of order-sorted equational programs modulo axioms
- Metalevel algorithms for variant satisfiability
- A modular order-sorted equational generalization algorithm
- Semantic foundations for generalized rewrite theories
- Algebraic and logic programming. Third international conference, ALP '92, Volterra, Italy, September 2--4, 1992. Proceedings
- Equational formulas and pattern operations in initial order-sorted algebras
- Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
- Deduction, Strategies, and Rewriting
- Modular Structural Operational Semantics with Strategies
- Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics
- Infinite-State Model Checking of LTLR Formulas Using Narrowing
- Two Decades of Maude
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Order-Sorted Parameterization and Induction
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
- The Temporal Logic of Rewriting: A Gentle Introduction
- Algorithm = logic + control
- Institutions: abstract model theory for specification and programming
- From Hoare Logic to Matching Logic Reachability
- Variant-Based Satisfiability in Initial Algebras
- Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
- Order-sorted Equational Unification Revisited
- Predicate Abstraction of Rewrite Theories
- All-Path Reachability Logic
- A Rewriting Semantics for Maude Strategies
- Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6
- Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
- Functional Logic Programming in Maude
- Strategies and simulations in a semantic framework
- Term Rewriting and Applications
- On sentences which are true of direct unions of algebras
- Equality, types, modules, and (why not?) generics for logic programming
- Rewriting logic as a semantic framework for concurrency: a progress report
- Associative unification and symbolic reasoning modulo associativity in Maude
- Proving structural properties of sequent systems in rewriting logic
- Generalized rewrite theories and coherence completion
