• Maude

  • Referenced in 650 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 26 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...
  • JPAX

  • Referenced in 29 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...
  • JavaFAN

  • Referenced in 30 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 38 articles [sw09970]
  • tool (http://www.lcc.uma.es/ duran/MTT/ ) for termination of Maude programs. CiME2 is no longer maintained...
  • MTT

  • Referenced in 21 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 16 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 16 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...
  • K tool

  • Referenced in 16 articles [sw09746]
  • interaction between the 𝕂 Tool and Maude...
  • ChC 3

  • Referenced in 11 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...
  • 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...
  • 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 9 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...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • this fragment as an equational theory in Maude. It supports compositional reasoning in a Hoare ... conditions (VCs) which are then sent to Maude’s Inductive Theorem Prover...
  • MOMENT2

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

  • Referenced in 4 articles [sw09764]
  • Maude Formal Environment (MFE) is an executable and highly extensible software infrastructure within which ... several tools to mechanically verify properties of Maude specifications. In MFE, tools can interoperate ... other features. MFE is naturally modeled in Maude as an object-based system in which ... passing. User interaction is available through Full Maude, an extension of Maude that has become...
  • 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...