Maude Tools

Formal tools for Maude specifications

• NuITP - An Inductive Theorem Prover for Maude Specifications]
• The Maude Formal Environment - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool
• The Maude LTLR Model Checker
• The Maude LTL Logical Model Checker
• umaudemc - A unified tool to check Maude specifications using external qualitative, probabilistic, and stochastical model checkers
• PVeStA - A Parallel Statistical Model Checking and Quantitative Analysis Tool
• MultiVeStA - A Distributed Statistical Model Checking for Discrete Event Simulators
• Inductive Theorem Prover (ITP)
• Sufficient Completeness Checker
• Maude-NPA - Maude-NRL Protocol Analyzer
• Equality Enrichments for Order-Sorted Maude Theories
• createCINNI - Automatic Generation of CINNI Instances for the Maude System

Extensions of Maude

• Real-Time Maude
• Maude Strategy Language
• ACUOS. Order-Sorted Modular ACU (Least General) Generalization System

Tools to assist in the development of Maude specifications

• Declarative Debugger
• The Anima tool - Stepwise inspection of Maude computations
• ABETS. Assertion-based, Maude dynamic analyzer
• iJulienne. Backward Trace Slicer

Tools for other formalisms and logics developed on Maude

• Pathway Logic Assistant - Modeling of biological entities and processes
• Circ - An automated behavioral prover based on the circularity principle
• OCC - An Open Calculus of Constructions
• CCS and LOTOS

Semantics and verification of programming languages

• Maude MSOS tool
• The K framework and Matching logic - Rewrite-based framework for the definition of formal operational semantics of programming languages
• JavaRL Rewriting specification of a Java semantics - Java interpreter and formal analysis
• JavaFAN - Executable rewrite logic semantics of both Java and Java Bytecode using Maude
• Java+ITP - A tool to prove Java properties

Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)

• MR-SynchAADL - Multirate Synchronous AADL and the MR-SynchAADL tool
• MOMENT - A framework for model management
• e-Motions - Visual definition of domain-specific modeling languages
• mOdCL - UML/OCL specification, with static and dynamic evaluation of OCL expressions
• Web-TLR. A Model Checker for Web applications using LTLR

Other tools

• Python's library Language bindings to use Maude from other programming languages like Python
• Maude Termination Tool
• Coherence Checker
• Inductive Theorem Prover (old version) with Web-ITP
• Church Rosser Checker
• ITP/OCL tool
• MSR cryptoprotocol specification language (paper)