• 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...
  • ITP/OCL

  • Referenced in 7 articles [sw02727]
  • class diagrams. It is written entirely in Maude making extensive use of its reflective capabilities...
  • Rascal

  • Referenced in 4 articles [sw05380]
  • including one showing integration with an existing Maude-based analysis. We then focus on ongoing ... used, and sketching a hypothetical solution in Maude. We conclude with a high-level discussion ... commonalities and differences between Rascal and Maude when applied to program analysis...
  • Pirlo

  • Referenced in 4 articles [sw08421]
  • methodology can be instantiated by considering the Maude implementation of SCEL and a specific reasoner ... Pirlo, implemented in Maude as well. Moreover we show how the actual integration can benefit ... from the existing analytical tools of the Maude framework. In particular, we demonstrate our approach...
  • AADL

  • Referenced in 4 articles [sw20835]
  • Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification into...
  • CafeInMaude

  • Referenced in 3 articles [sw19598]
  • CafeInMaude: A CafeOBJ Interpreter in Maude. We present in this paper CafeInMaude, an interpreter ... specifications. The interpreter has been implemented in Maude. This alternative implementation combines CafeOBJ specification ... theorem proving capabilities with efficient and extensible Maude commands and tools. Hence, it makes ... CafeOBJ proof scores and reduction commands and Maude model checking, narrowing, or theorem proving capabilities...
  • tccp

  • Referenced in 3 articles [sw28619]
  • result of implementing the tccp language in Maude. Maude has been shown to be well ... behavior, also allowing us to reuse the Maude features to execute and analyze tccp programs...
  • BMaude

  • Referenced in 2 articles [sw10135]
  • Towards behavioral Maude: behavioral membership equational logic. How can algebraic and coalgebraic specifications be integrated ... hidden logic, and an extension of the Maude specification language called BMaude supporting this extended ... hidden-sorted semantics.par Maude’s underlying equational logic, membership equational logic, generalizes and increases ... different institutions involved. We also explain how Maude’s reflective semantics provides a systematic method...
  • Petri-PDL

  • Referenced in 3 articles [sw15081]
  • prototype implementation, in the Rewriting Logic language Maude, of a bounded model checker for Petri ... Temporal Logic model checker available in the Maude system...
  • SynchAADL2Maude

  • Referenced in 4 articles [sw13325]
  • Eclipse plug-in that uses Real-Time Maude to simulate and model check Synchronous AADL...
  • DeltaCCS

  • Referenced in 4 articles [sw14476]
  • DeltaCCS model checker implementation based on {sc Maude} and provide evaluation results obtained from various...
  • ATAME

  • Referenced in 2 articles [sw25797]
  • Inferring Safe Maude Programs with ÁTAME. In this paper, we present ÁTAME, an assertion-based ... specialization tool for the multi-paradigm language Maude. The program specializer ÁTAME takes as input ... model the expected program behavior plus a Maude program R to be specialized that might...
  • InvA

  • Referenced in 2 articles [sw10124]
  • alternating bit protocol using the maude invariant analyzer tool. The InvA tool supports the deductive ... automation, verifying automatically many proof obligations. Maude inductive theorem prover (ITP) can be used...
  • PSMaude

  • Referenced in 3 articles [sw10125]
  • have implemented PSMaude, a tool that extends Maude with a probabilistic simulator and a statistical...
  • ABETS

  • Referenced in 3 articles [sw31985]
  • dynamic analyzer that helps diagnose errors in Maude programs. ABETS uses slicing to automatically create...
  • CBabel

  • Referenced in 2 articles [sw07520]
  • verification of CBabel descriptions in the Maude system, an implementation of rewriting logic. In this...
  • Mumbo

  • Referenced in 1 article [sw07651]
  • achieve actual optimization. The model, written in Maude, preserves all the essential ingredients of Jumbo ... simplification in the language together with Maude’s support for code rewriting has allowed...
  • ACL2

  • Referenced in 277 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1776 articles [sw00161]
  • Coq is a formal proof management system. It...