• Maude

  • Referenced in 614 articles [sw06233]
  • Maude is a high-performance reflective language and system supporting both equational and rewriting logic ... programming for a wide range of applications. Maude has been influenced in important ways ... sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation...
  • Maude-NPA

  • Referenced in 22 articles [sw12159]
  • State space reduction in the Maude-NRL protocol analyzer. The Maude-NRL Protocol Analyzer (Maude ... equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic ... example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks ... reduction techniques that we have implemented in Maude-NPA. We also provide completeness proofs...
  • JavaFAN

  • Referenced in 29 articles [sw01934]
  • consists of only 3,000 lines of Maude code, specifying formally the semantics of Java ... logic and then using the capabilities of Maude for efficient execution, search and LTL model...
  • CiME

  • Referenced in 37 articles [sw09970]
  • tool (http://www.lcc.uma.es/ duran/MTT/ ) for termination of Maude programs. CiME2 is no longer maintained...
  • MTT

  • Referenced in 20 articles [sw09783]
  • Maude termination tool. Despite the remarkable development of the theory of termination of rewriting ... heart of the most recent formulation of Maude...
  • MMT

  • Referenced in 15 articles [sw07905]
  • Maude MSOS tool. Modular structural operational semantics (MSOS) is a new framework that allows structural ... specifications, when an extension is made. Maude MSOS tool (MMT) is an executable environment ... MSOS implemented in Full Maude as a realization of a semantics-preserving mapping between MSOS ... efficient execution and analysis of the Maude engine. We have used MMT in several different...
  • PVeStA

  • Referenced in 15 articles [sw08423]
  • scalability of analysis available to tools like Maude, where probabilistic systems can be specified ... Chains; or (ii) probabilistic rewrite theories in Maude. Furthermore, the properties that it can model...
  • DDebugger

  • Referenced in 15 articles [sw09904]
  • proved. Using these trees we have implemented Maude DDebugger, a declarative debugger for Maude...
  • K-Maude

  • Referenced in 10 articles [sw09747]
  • Maude: A rewriting based tool for semantics of programming languages. K is a rewriting-based ... framework for defining programming languages. K-Maude is a tool implementing ... Maude. K-Maude provides an interface accepting K modules along with regular Maude modules ... tools for transforming K language definitions into Maude rewrite theories for execution or analysis...
  • SCC

  • Referenced in 11 articles [sw09809]
  • tool for partial specifications. We present the Maude sufficient completeness tool, which explicitly supports sufficient ... discharged, ensures sufficient completeness; and (ii) Maude’s inductive theorem prover (ITP) that is used...
  • K tool

  • Referenced in 15 articles [sw09746]
  • interaction between the 𝕂 Tool and Maude...
  • JPAX

  • Referenced in 9 articles [sw09906]
  • formulated by the user in the Maude rewriting logic, where Maude is a high-speed ... here extended with executable temporal logic. The Maude rewriting engine is then activated...
  • ChC 3

  • Referenced in 10 articles [sw09781]
  • Maude coherence checker tool for conditional order-sorted rewrite theories. For a rewrite theory ... present the mathematical foundations of the Maude ChC 3 tool, which provide such a generalization...
  • CARIBOO

  • Referenced in 14 articles [sw10064]
  • applies to languages such as ASF+SDF, Maude, Cafe-OBJ, or ELAN. By contrast with...
  • CRC 3

  • Referenced in 8 articles [sw09782]
  • checker tool for conditional order-sorted equational Maude specifications. The Church-Rosser property, together with ... completely new version of the Maude Church-Rosser Checker tool that addresses all the above...
  • MOMENT2

  • Referenced in 10 articles [sw10025]
  • simulated and model checked using MOMENT2’s Maude-based analysis tools. In this way, MOMENT2...
  • Web-TLR

  • Referenced in 8 articles [sw09905]
  • formally verified by using the Maude built-in LTLR model-checker. Web-TLR is equipped...
  • HI-maude

  • Referenced in 4 articles [sw09753]
  • maude tool. In complex hybrid systems, different components may influence each others’ continuous behaviors ... Maude is a rewriting-logic-based tool that supports an object-oriented modeling methodology ... objects in such interacting hybrid systems. HI-Maude supports simulation and model checking...
  • iJulienne

  • Referenced in 5 articles [sw09903]
  • used to compute abstract views of Maude executions that help users understand and debug programs ... Given a Maude execution trace and a slicing criterion which consists...
  • Dist-Orc

  • Referenced in 5 articles [sw10063]
  • implementation technique based on rewriting logic and Maude that narrows this gap considerably. The enabling ... feature of this technique is Maude’s support for external objects through TCP sockets...