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)
- 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
- Maude
- Algebraic simulations
- How to prove decidability of equational theories with second-order computation analyser SOL
- Order-sorted generalization
- Abstract Certification of Global Non-interference in Rewriting Logic
- Completeness of context-sensitive rewriting
- Integrating deployment architectures and resource consumption in timed object-oriented models
- SOS rule formats for idempotent terms and idempotent unary operators
- Equational abstractions
- Exploring conditional rewriting logic computations
- Using the Maude term rewriting language for agent development with formal foundations
- Amalgamation of domain specific languages with behaviour
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Rewriting modulo SMT and open system analysis
- Circular coinduction: a proof theoretical foundation
- Title not available (Why is that?)
- A declarative debugger for Maude functional modules
- HasCasl: integrated higher-order specification and program development
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- Comparing three coordination models: Reo, ARC, and PBRD
- Efficient general unification for XOR with homomorphism
- An overview of the K semantic framework
- Normal forms and normal theories in conditional rewriting
- Termination criteria for tree automata completion
- A formal library of set relations and its application to synchronous languages
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Context-sensitive dependency pairs
- A language-based approach to modelling and analysis of Twitter interactions
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- Language definitions as rewrite theories
- A Maude environment for CafeOBJ
- ACUOS: a system for modular ACU generalization with subtyping and inheritance
- The \textsf{tccp} interpreter
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Declarative debugging of rewriting logic specifications
- Proving termination properties with \textsc{mu-term}
- 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
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)
