Maude
From MaRDI portal
Software:18367
No author found.
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Maude: specification and programming in rewriting logic
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Unnamed Publication
Related Items (only showing first 100 items - show all)
A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Rewriting logic: Roadmap and bibliography ⋮ An overview of the runtime verification tool Java PathExplorer ⋮ Strategies for combining decision procedures ⋮ Executable structural operational semantics in Maude ⋮ Structured theories and institutions ⋮ Equational logic and categorical semantics for multi-languages ⋮ Order-sorted equational generalization algorithm revisited ⋮ The transient combinator, higher-order strategies, and the distributed data problem ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Hardware Trojan detection via rewriting logic ⋮ On the collective sort problem for distributed tuple spaces ⋮ Upward refinement operators for conceptual blending in the description logic \(\mathcal{EL}^{++}\) ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Inferring safe Maude programs with ÁTAME ⋮ A formal proof generator from semi-formal proof documents ⋮ Executing and verifying higher-order functional-imperative programs in Maude ⋮ Partial evaluation of order-sorted equational programs modulo axioms ⋮ Birkhoff completeness for hybrid-dynamic first-order logic ⋮ Improved support vector machine algorithm for heterogeneous data ⋮ Metalevel algorithms for variant satisfiability ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ On the accuracy of formal verification of selective defenses for TDoS attacks ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Declarative debugging of rewriting logic specifications ⋮ Folding variant narrowing and optimal variant termination ⋮ Rewriting semantics of production rule sets ⋮ Typed generic traversal with term rewriting strategies ⋮ Specification and verification of the tree identify protocol of IEEE 1394 in rewriting logic ⋮ On combining algebraic specifications with first-order logic via Athena ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ 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 ⋮ Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system ⋮ Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9--11, 2003. Proceedings ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Algebraic models of correctness for abstract pipelines. ⋮ Leveraging the information contained in theory presentations ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Executable component-based semantics ⋮ Specification and proof in membership equational logic ⋮ Formalizing and analyzing security ceremonies with heterogeneous devices in ANP and PDL ⋮ Travelling salesman problem in tissue P systems with costs ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Resource provisioning strategies for BPMN processes: specification and analysis using Maude ⋮ Synchronous products of rewrite systems ⋮ Symbolic execution based on language transformation ⋮ Automated deduction and knowledge management in geometry ⋮ Well-structuredness, safeness and soundness: a formal classification of BPMN collaborations ⋮ Proving operational termination of membership equational programs ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ Verification of multi-agent systems with timeouts for migration and communication ⋮ Variadic equational matching in associative and commutative theories ⋮ Data-driven modeling of Alzheimer disease pathogenesis ⋮ Fast machine words in Isabelle/HOL ⋮ CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications ⋮ Proving semantic properties as first-order satisfiability ⋮ A coinductive approach to proving reachability properties in logically constrained term rewriting systems ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ A formal approach to the engineering of domain-specific distributed systems ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Explaining safety failures in NetKAT ⋮ Applications and extensions of context-sensitive rewriting ⋮ \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance ⋮ Using well-founded relations for proving operational termination ⋮ Finding intruder knowledge with cap-matching ⋮ Symbolic timed trace equivalence ⋮ Automatic generation of logical models with AGES ⋮ Analysing an autonomous tramway positioning system with the \textsc{Uppaal} statistical model checker ⋮ Derivational complexity and context-sensitive Rewriting ⋮ ROLA: a new distributed transaction protocol and its formal analysis ⋮ A semantic model for interacting cyber-physical systems ⋮ Dynamic structural operational semantics ⋮ Reasoning about block-based cloud storage systems via separation logic ⋮ 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 ⋮ Bounded memory protocols ⋮ Normal forms for algebras of connections. ⋮ Automata-driven automated induction ⋮ Functorial models for Petri nets ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs ⋮ Dynamic connectors for concurrency ⋮ ELAN from a rewriting logic point of view ⋮ Reflection in conditional rewriting logic ⋮ Logical foundations of CafeOBJ ⋮ Comparing logics for rewriting: Rewriting logic, action calculi and tile logic ⋮ Specification of real-time and hybrid systems in rewriting logic ⋮ A Maude specification of an object-oriented model for telecommunication networks ⋮ Actor theories in rewriting logic ⋮ Equational rules for rewriting logic ⋮ A formal approach to object-oriented software engineering ⋮ Symbolic computation in Maude: some tapas ⋮ Runtime complexity analysis of logically constrained rewriting ⋮ Pattern eliminating transformations
This page was built for software: Maude
