All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
From MaRDI portal
Publication:997833
zbMATH Open1115.68046MaRDI QIDQ997833FDOQ997833
Authors: M. Clavel, Francisco Durán, Steven Eker, Narciso Martí-Oliet, José Meseguer, P. Lincoln, Carolyn Talcott 
Publication date: 8 August 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Recommendations
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Distributed systems (68M14)
Cited In (only showing first 100 items - show all)
- A Modular Equational Generalization Algorithm
- Strict coherence of conditional rewriting modulo axioms
- Equational formulas and pattern operations in initial order-sorted algebras
- Equational formulas and pattern operations in initial order-sorted algebras
- An evaluation of interaction paradigms for active objects
- An executable semantics of clock constraint specification language and its applications
- Structural induction in institutions
- P systems with control nuclei: the concept
- Termination of narrowing revisited
- Formalization and correctness of the PALS architectural pattern for distributed real-time systems
- Complexity of conditional term rewriting
- Symbolic execution based on language transformation
- Closure via functional dependence simplification
- On-demand strategy annotations revisited: an improved on-demand evaluation strategy
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Runtime complexity analysis of logically constrained rewriting
- Modeling and analyzing mobile ad hoc networks in Real-Time Maude
- Automated deduction and knowledge management in geometry
- A process calculus BigrTiMo of mobile systems and its formal semantics
- Strategy-based proof calculus for membrane systems
- Applications and extensions of context-sensitive rewriting
- A formalisation of deep metamodelling
- Debugging Maude programs via runtime assertion checking and trace slicing
- Invariant-driven specifications in Maude
- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Compositional reasoning about active objects with shared futures
- Use of logical models for proving operational termination in general logics
- Constructor-based institutions
- A complete declarative debugger for Maude
- Data-driven modeling of Alzheimer disease pathogenesis
- A rewriting semantics for Maude strategies
- On the Specification and Verification of Model Transformations
- What Is a Multi-modeling Language?
- Formal analysis of leader election in MANETs using Real-Time Maude
- Symbolic reasoning methods in rewriting logic and Maude
- Backward trace slicing for rewriting logic theories
- Combining runtime checking and slicing to improve Maude error diagnosis
- From rewriting logic, to programming language semantics, to program verification
- Termination Modulo Combinations of Equational Theories
- Replicated data types that unify eventual consistency and observable atomic consistency
- On the accuracy of formal verification of selective defenses for TDoS attacks
- Order-Sorted Parameterization and Induction
- Using context-sensitive rewriting for proving innermost termination of rewriting
- Executable rewriting logic semantics of Orc and formal analysis of Orc programs
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- Interpreting abstract interpretations in membership equational logic
- A modular order-sorted equational generalization algorithm
- Variant-Based Satisfiability in Initial Algebras
- Title not available (Why is that?)
- A probabilistic approximate logic for neuro-symbolic learning and reasoning
- Order-Sorted Rewriting and Congruence Closure
- Derivational complexity and context-sensitive Rewriting
- Checking Sufficient Completeness by Inductive Theorem Proving
- A formal approach to the engineering of domain-specific distributed systems
- Bounded ACh unification
- Declarative Debugging of Membership Equational Logic Specifications
- Formalizing and analyzing security ceremonies with heterogeneous devices in ANP and PDL
- Compositional specification in rewriting logic
- The rewriting logic semantics project: a progress report
- The rewriting logic semantics project: a progress report
- Operational termination of conditional rewriting with built-in numbers and semantic data structures
- Operational termination of membership equational programs: the order-sorted way
- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- Twenty years of rewriting logic
- Multiset rewriting for the verification of depth-bounded processes with name binding
- Simulation and verification of synchronous set relations in rewriting logic
- A rewriting framework and logic for activities subject to regulations
- Automatic generation of logical models with AGES
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Rewriting-based repairing strategies for XML repositories
- A timed semantics of Orc
- An algebraic semantics for MOF
- A rewriting logic approach to operational semantics
- Rewriting strategies and strategic rewrite programs
- Automatic synthesis of logical models for order-sorted first-order theories
- A functional framework for agent-based models of exchange
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- Rewriting semantics of production rule sets
- Declarative Debugging of Rewriting Logic Specifications
- Matching logic: an alternative to Hoare/Floyd logic
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- A rewriting-based model checker for the linear temporal logic of rewriting
- Verifying hierarchical Ptolemy II discrete-event models using real-time maude
- Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
- Formal modeling and validation of a power-efficient grouping protocol for WSNs
- MTT: The Maude Termination Tool (System Description)
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- Title not available (Why is that?)
- An integrated framework for the diagnosis and correction of rule-based programs
- Coinduction for preordered algebra
- Programming in biomolecular computation
- Weak bisimulation as a congruence in MSOS
- A generic framework for \(n\)-protocol compatibility checking
- Assertion-based analysis via slicing withABETS(system description)
- Efficient general AGH-unification
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- Integrating Maude into Hets
- A compact fixpoint semantics for term rewriting systems
- Methods for proving termination of rewriting-based programming languages by transformation
Uses Software
This page was built for publication: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q997833)
