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
zbMath1115.68046MaRDI QIDQ997833
Manuel Clavel, Narciso Martí-Oliet, Francisco Durán, Steven Eker, José Meseguer, Carolyn L. Talcott, Patrick D. Lincoln
Publication date: 8 August 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Theory of programming languages (68N15) Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Distributed systems (68M14) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Equational logic and categorical semantics for multi-languages, Invariant-driven specifications in Maude, Equational formulas and pattern operations in initial order-sorted algebras, The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors, Hardware Trojan detection via rewriting logic, Algebraic simulations, On the complexity of verification of time-sensitive distributed systems, Joshua Guttman: pioneering strand spaces, Sentence-normalized conditional narrowing modulo in rewriting logic and Maude, Automatic synthesis of logical models for order-sorted first-order theories, 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, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, An integrated framework for the diagnosis and correction of rule-based programs, Executing and verifying higher-order functional-imperative programs in Maude, A probabilistic approximate logic for neuro-symbolic learning and reasoning, Metalevel transformation of strategies, Comparing three coordination models: Reo, ARC, and PBRD, Metalevel algorithms for variant satisfiability, Introducing \(H\), an institution-based formal specification and verification language, The rewriting logic semantics project: a progress report, On the accuracy of formal verification of selective defenses for TDoS attacks, Parameterized strategies specification in Maude, Twenty years of rewriting logic, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Declarative debugging of rewriting logic specifications, Rewriting semantics of production rule sets, Compositional reasoning about active objects with shared futures, Coinduction for preordered algebra, A functional framework for agent-based models of exchange, A generic framework for \(n\)-protocol compatibility checking, Rewriting-based repairing strategies for XML repositories, SOS rule formats for idempotent terms and idempotent unary operators, Verifying hierarchical Ptolemy II discrete-event models using real-time maude, A modular order-sorted equational generalization algorithm, Formal modeling and validation of a power-efficient grouping protocol for WSNs, Stability of termination and sufficient-completeness under pushouts via amalgamation, Efficient general AGH-unification, A symbolic transformation language and its application to a multiscale method, A formal library of set relations and its application to synchronous languages, Completeness of context-sensitive rewriting, Integrating deployment architectures and resource consumption in timed object-oriented models, The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques, A timed semantics of Orc, Exploring conditional rewriting logic computations, An evaluation of interaction paradigms for active objects, Program equivalence by circular reasoning, Formalizing and analyzing security ceremonies with heterogeneous devices in ANP and PDL, Equational abstractions, \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages, Strategies, model checking and branching-time properties in Maude, Resource provisioning strategies for BPMN processes: specification and analysis using Maude, A generic framework for symbolic execution: a coinductive approach, A language-based approach to modelling and analysis of Twitter interactions, Symbolic execution based on language transformation, Strict coherence of conditional rewriting modulo axioms, A Maude environment for CafeOBJ, Automated deduction and knowledge management in geometry, An algebraic semantics for MOF, Multiset rewriting for the verification of depth-bounded processes with name binding, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, P systems with control nuclei: the concept, An overview of the K semantic framework, A compact fixpoint semantics for term rewriting systems, Structural induction in institutions, Context-sensitive dependency pairs, A process calculus BigrTiMo of mobile systems and its formal semantics, Variadic equational matching in associative and commutative theories, Data-driven modeling of Alzheimer disease pathogenesis, Termination criteria for tree automata completion, Modeling and analyzing mobile ad hoc networks in Real-Time Maude, Normal forms and normal theories in conditional rewriting, Language definitions as rewrite theories, Proving semantic properties as first-order satisfiability, Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, A formalisation of deep metamodelling, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, A formal approach to the engineering of domain-specific distributed systems, Ground confluence of order-sorted conditional specifications modulo axioms, HasCasl: integrated higher-order specification and program development, Applications and extensions of context-sensitive rewriting, Debugging Maude programs via runtime assertion checking and trace slicing, A rewriting logic approach to operational semantics, Using well-founded relations for proving operational termination, Automatic generation of logical models with AGES, Maude, Derivational complexity and context-sensitive Rewriting, Termination of narrowing revisited, A semantic model for interacting cyber-physical systems, Replicated data types that unify eventual consistency and observable atomic consistency, On-demand strategy annotations revisited: an improved on-demand evaluation strategy, Read atomic transactions with prevention of lost updates: ROLA and its formal analysis, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Composition of multilevel domain-specific modelling languages, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Executable rewriting logic semantics of Orc and formal analysis of Orc programs, Symbolic computation in Maude: some tapas, Runtime complexity analysis of logically constrained rewriting, Symbolic Specialization of Rewriting Logic Theories with Presto, Variants and satisfiability in the infinitary unification wonderland, The Maude strategy language, Modular rewritable Petri nets: an efficient model for dynamic distributed systems, Local confluence of conditional and generalized term rewriting systems, Formal modeling of multi-viewpoint ontology alignment by mappings composition, Session-based concurrency in Maude: executable semantics and type checking, Canonization of reconfigurable PT nets in \texttt{Maude}, QMaude: quantitative specification and verification in rewriting logic, DyNetKAT: an algebra of dynamic networks, Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K, Circular Coinduction: A Proof Theoretical Foundation, Constructor-Based Institutions, Building a Modal Interface Theory for Concurrency and Data, A New Strategy for Distributed Compensations with Interruption in Long-Running Transactions, Combining Graph Transformation and Algebraic Specification into Model Transformation, Detection and diagnosis of deviations in distributed systems of autonomous agents, Unnamed Item, mu-term: Verify Termination Properties Automatically (System Description), Probabilistic Real-Time Rewrite Theories and Their Expressive Power, Model Checking Security Protocols, A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler, What Is a Multi-modeling Language?, Declarative Debugging of Rewriting Logic Specifications, Order-Sorted Parameterization and Induction, On the Specification and Verification of Model Transformations, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance, Optimization of rewrite theories by equational partial evaluation, José Meseguer: Scientist and Friend Extraordinaire, Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude, Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis, Alice and Bob Meet Equational Theories, Two Decades of Maude, Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting, Rewriting Strategies and Strategic Rewrite Programs, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, Weak Bisimulation as a Congruence in MSOS, Algebraic Reinforcement Learning, From Rewriting Logic, to Programming Language Semantics, to Program Verification, CLP(H):Constraint logic programming for hedges, Assertion-based analysis via slicing withABETS(system description), Symbolic Analysis of Maude Theories with Narval, Compositional Specification in Rewriting Logic, Graph-Based Design and Analysis of Dynamic Software Architectures, Declarative Debugging of Membership Equational Logic Specifications, How to prove decidability of equational theories with second-order computation analyser SOL, Verification of the ROS NavFn planner using executable specification languages, A rewriting framework and logic for activities subject to regulations, Unnamed Item, Unnamed Item, Unnamed Item, Towards Modelling Actor-Based Concurrency in Term Rewriting, MTT: The Maude Termination Tool (System Description), Bounded ACh unification, A Decision Procedure for Bisimilarity of Generalized Regular Expressions, Closure via functional dependence simplification, CafeOBJ Traces, Model Checking TLR* Guarantee Formulas on Infinite Systems, Functional Logic Programming in Maude, An Institution for Imperative RSL Specifications, Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method, On Automation of OTS/CafeOBJ Method, Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs, Programming in Biomolecular Computation, A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures, The tccp Interpreter, Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras, Memory Policy Analysis for Semantics Specifications in Maude, Strategy-Based Proof Calculus for Membrane Systems, Hierarchical Design Rewriting with Maude, A Declarative Debugger for Maude Functional Modules, Patterns for Maude Metalanguage Applications, Operational Termination of Membership Equational Programs: the Order-Sorted Way, A Rewriting Semantics for Maude Strategies, Combining Techniques to Reduce State Space and Prove Strong Properties, Coordinating Asynchronous and Open Distributed Systems under Semiring-Based Timing Constraints, Unnamed Item, Variant-Based Satisfiability in Initial Algebras, An Executable Semantics of Clock Constraint Specification Language and Its Applications, Backward Trace Slicing for Rewriting Logic Theories, Efficient General Unification for XOR with Homomorphism, Equational Abstractions in Rewriting Logic and Maude, Abstract Certification of Global Non-interference in Rewriting Logic, Integrating Maude into Hets, Matching Logic: An Alternative to Hoare/Floyd Logic, Proving Termination Properties with mu-term, A Complete Declarative Debugger for Maude, Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints, A Modular Equational Generalization Algorithm, Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting, Methods for Proving Termination of Rewriting-based Programming Languages by Transformation, Order-Sorted Rewriting and Congruence Closure, Built-in Variant Generation and Unification, and Their Applications in Maude 2.7, The Rewriting Logic Semantics Project: A Progress Report, REWRITING LOGIC-BASED SEMANTICS OF P SYSTEMS AND THE MAXIMAL CONCURRENCY, Use of Logical Models for Proving Operational Termination in General Logics, Proving Reachability-Logic Formulas Incrementally, Metalevel Algorithms for Variant Satisfiability, Simulation and Verification of Synchronous Set Relations in Rewriting Logic, Order-Sorted Generalization, Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework, Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*, Termination Modulo Combinations of Equational Theories, Interpreting Abstract Interpretations in Membership Equational Logic, Towards Behavioral Maude, Formal Analysis of Leader Election in MANETs Using Real-Time Maude, Soft Agents: Exploring Soft Constraints to Model Robust Adaptive Distributed Cyber-Physical Agent Systems, A White Box Perspective on Behavioural Adaptation
Uses Software
